<html>
<head><title>The dddmp package: all functions </title></head>
<body>

A set of internal low-level routines of the dddmp package
    doing:
    <ul>
      <li> read and write of node codes in binary mode,
      <li> read and write of integers in binary mode,
      <li> marking/unmarking nodes as visited,
      <li> numbering nodes.
    </ul>
<HR>
<DL>
<dt><pre>
<A NAME="DddmpBddReadHeaderCnf"></A>
static Dddmp_Hdr_t * <I></I>
<B>DddmpBddReadHeaderCnf</B>(
  char * <b>file</b>, <i>IN: file name</i>
  FILE * <b>fp</b> <i>IN: file pointer</i>
)
</pre>
<dd> Reads the header of a dump file. Builds a Dddmp_Hdr_t struct
    containing all infos in the header, for next manipulations.
<p>

<dd> <b>Side Effects</b> none
<p>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpLoadCnf.c"TARGET="ABSTRACT"><CODE>dddmpLoadCnf.c</CODE></A>

<dt><pre>
<A NAME="DddmpBddReadHeader"></A>
static Dddmp_Hdr_t * <I></I>
<B>DddmpBddReadHeader</B>(
  char * <b>file</b>, <i>IN: file name</i>
  FILE * <b>fp</b> <i>IN: file pointer</i>
)
</pre>
<dd> Reads the header of a dump file. Builds a Dddmp_Hdr_t struct
    containing all infos in the header, for next manipulations.
<p>

<dd> <b>Side Effects</b> none
<p>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpLoad.c"TARGET="ABSTRACT"><CODE>dddmpLoad.c</CODE></A>

<dt><pre>
<A NAME="DddmpClearVisitedAdd"></A>
void <I></I>
<B>DddmpClearVisitedAdd</B>(
  DdNode * <b>f</b> <i>IN: BDD node to be marked (as not visited)</i>
)
</pre>
<dd> Marks a node as not visited
<p>

<dd> <b>Side Effects</b> None
<p>

<dd> <b>See Also</b> <code><a href="#DddmpVisitedAdd">DddmpVisitedAdd</a>
()
<a href="#DddmpSetVisitedAdd">DddmpSetVisitedAdd</a>
()
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeAdd.c"TARGET="ABSTRACT"><CODE>dddmpNodeAdd.c</CODE></A>

<dt><pre>
<A NAME="DddmpClearVisitedBdd"></A>
void <I></I>
<B>DddmpClearVisitedBdd</B>(
  DdNode * <b>f</b> <i>IN: BDD node to be marked (as not visited)</i>
)
</pre>
<dd> Marks a node as not visited
<p>

<dd> <b>Side Effects</b> None
<p>

<dd> <b>See Also</b> <code><a href="#DddmpVisited">DddmpVisited</a>
()
<a href="#DddmpSetVisited">DddmpSetVisited</a>
()
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeBdd.c"TARGET="ABSTRACT"><CODE>dddmpNodeBdd.c</CODE></A>

<dt><pre>
<A NAME="DddmpClearVisitedCnfRecur"></A>
static int <I></I>
<B>DddmpClearVisitedCnfRecur</B>(
  DdNode * <b>f</b> <i>IN: root of the BDD to be marked</i>
)
</pre>
<dd> Mark ALL nodes as not visited (it recurs on the node children)
<p>

<dd> <b>Side Effects</b> None
<p>

<dd> <b>See Also</b> <code><a href="#DddmpVisitedCnf">DddmpVisitedCnf</a>
()
<a href="#DddmpSetVisitedCnf">DddmpSetVisitedCnf</a>
()
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeCnf.c</CODE></A>

<dt><pre>
<A NAME="DddmpClearVisitedCnfRecur"></A>
static int <I></I>
<B>DddmpClearVisitedCnfRecur</B>(
  DdNode * <b>f</b> <i>IN: root of the BDD to be marked</i>
)
</pre>
<dd> Mark ALL nodes as not visited (it recurs on the node children)
<p>

<dd> <b>Side Effects</b> None
<p>

<dd> <b>See Also</b> <code><a href="#DddmpVisitedCnf">DddmpVisitedCnf</a>
()
<a href="#DddmpSetVisitedCnf">DddmpSetVisitedCnf</a>
()
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpNodeCnf.c</CODE></A>

<dt><pre>
<A NAME="DddmpClearVisitedCnf"></A>
static void <I></I>
<B>DddmpClearVisitedCnf</B>(
  DdNode * <b>f</b> <i>IN: BDD node to be marked (as not visited)</i>
)
</pre>
<dd> Marks a node as not visited
<p>

<dd> <b>Side Effects</b> None
<p>

<dd> <b>See Also</b> <code><a href="#DddmpVisitedCnf">DddmpVisitedCnf</a>
()
<a href="#DddmpSetVisitedCnf">DddmpSetVisitedCnf</a>
()
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeCnf.c</CODE></A>

<dt><pre>
<A NAME="DddmpClearVisitedCnf"></A>
static void <I></I>
<B>DddmpClearVisitedCnf</B>(
  DdNode * <b>f</b> <i>IN: BDD node to be marked (as not visited)</i>
)
</pre>
<dd> Marks a node as not visited
<p>

<dd> <b>Side Effects</b> None
<p>

<dd> <b>See Also</b> <code><a href="#DddmpVisitedCnf">DddmpVisitedCnf</a>
()
<a href="#DddmpSetVisitedCnf">DddmpSetVisitedCnf</a>
()
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpNodeCnf.c</CODE></A>

<dt><pre>
<A NAME="DddmpClearVisited"></A>
void <I></I>
<B>DddmpClearVisited</B>(
  DdNode * <b>f</b> <i>IN: BDD node to be marked (as not visited)</i>
)
</pre>
<dd> Marks a node as not visited
<p>

<dd> <b>Side Effects</b> None
<p>

<dd> <b>See Also</b> <code><a href="#DddmpVisited">DddmpVisited</a>
()
<a href="#DddmpSetVisited">DddmpSetVisited</a>
()
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeBdd.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeBdd.c</CODE></A>

<dt><pre>
<A NAME="DddmpCnfClauses2Bdd"></A>
static int <I></I>
<B>DddmpCnfClauses2Bdd</B>(
  Dddmp_Hdr_t * <b>Hdr</b>, <i>IN: file header</i>
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  int ** <b>cnfTable</b>, <i>IN: CNF table for clauses</i>
  int  <b>mode</b>, <i>IN: computation mode</i>
  DdNode *** <b>rootsPtrPtr</b> <i>OUT: array of returned BDD roots (by reference)</i>
)
</pre>
<dd> Transforms CNF clauses into BDDs. Clauses are stored in an
   internal structure previously read. The results can be given in
   different format according to the mode selection:
     IFF mode == 0 Return the Clauses without Conjunction
     IFF mode == 1 Return the sets of BDDs without Quantification
     IFF mode == 2 Return the sets of BDDs AFTER Existential Quantification
<p>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpLoadCnf.c"TARGET="ABSTRACT"><CODE>dddmpLoadCnf.c</CODE></A>

<dt><pre>
<A NAME="DddmpCuddBddArrayStoreCnf"></A>
static int <I></I>
<B>DddmpCuddBddArrayStoreCnf</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  DdNode ** <b>f</b>, <i>IN: array of BDD roots to be stored</i>
  int  <b>rootN</b>, <i>IN: # of output BDD roots to be stored</i>
  Dddmp_DecompCnfStoreType  <b>mode</b>, <i>IN: format selection</i>
  int  <b>noHeader</b>, <i>IN: do not store header iff 1</i>
  char ** <b>varNames</b>, <i>IN: array of variable names (or NULL)</i>
  int * <b>bddIds</b>, <i>IN: array of BDD node Ids (or NULL)</i>
  int * <b>bddAuxIds</b>, <i>IN: array of BDD Aux Ids (or NULL)</i>
  int * <b>cnfIds</b>, <i>IN: array of CNF ids (or NULL)</i>
  int  <b>idInitial</b>, <i>IN: starting id for cutting variables</i>
  int  <b>edgeInTh</b>, <i>IN: Max # Incoming Edges</i>
  int  <b>pathLengthTh</b>, <i>IN: Max Path Length</i>
  char * <b>fname</b>, <i>IN: file name</i>
  FILE * <b>fp</b>, <i>IN: pointer to the store file</i>
  int * <b>clauseNPtr</b>, <i>OUT: number of clause stored</i>
  int * <b>varNewNPtr</b> <i>OUT: number of new variable created</i>
)
</pre>
<dd> Dumps the argument array of BDDs/ADDs to file in CNF format.
    The following arrays: varNames, bddIds, bddAuxIds, and cnfIds 
    fix the correspondence among variable names, BDD ids, BDD 
    auxiliary ids and the ids used to store the CNF problem.
    All these arrays are automatically created iff NULL.
    Auxiliary variable, iff necessary, are created starting from value
    idInitial.
    Iff idInitial is <= 0 its value is selected as the number of internal
    CUDD variable + 2.
    Auxiliary variables, i.e., cut points are inserted following these
    criterias:
    * edgeInTh
      indicates the maximum number of incoming edges up to which
      no cut point (auxiliary variable) is inserted.
      If edgeInTh:
      * is equal to -1 no cut point due to incoming edges are inserted
        (MaxtermByMaxterm method.)
	* is equal to 0 a cut point is inserted for each node with a single
        incoming edge, i.e., each node, (NodeByNode method).
	* is equal to n a cut point is inserted for each node with (n+1)
        incoming edges.
    * pathLengthTh
      indicates the maximum length path up to which no cut points
      (auxiliary variable) is inserted.
      If the path length between two nodes exceeds this value, a cut point
      is inserted.
      If pathLengthTh:
      * is equal to -1 no cut point due path length are inserted
        (MaxtermByMaxterm method.)
	* is equal to 0 a cut point is inserted for each node (NodeByNode
        method).
	* is equal to n a cut point is inserted on path whose length is
        equal to (n+1).
      Notice that the maximum number of literals in a clause is equal
      to (pathLengthTh + 2), i.e., for each path we have to keep into
      account a CNF variable for each node plus 2 added variables for
      the bottom and top-path cut points.
<p>

<dd> <b>Side Effects</b> Nodes are temporarily removed from the unique hash table. 
    They are re-linked after the store operation in a modified 
    order.
<p>

<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddStore">Dddmp_cuddBddStore</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreCnf.c"TARGET="ABSTRACT"><CODE>dddmpStoreCnf.c</CODE></A>

<dt><pre>
<A NAME="DddmpCuddBddArrayStore"></A>
int <I></I>
<B>DddmpCuddBddArrayStore</B>(
  Dddmp_DecompType  <b>ddType</b>, <i>IN: Selects the decomp type BDD</i>
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  char * <b>ddname</b>, <i>IN: DD name (or NULL)</i>
  int  <b>nRoots</b>, <i>IN: number of output BDD roots to be stored</i>
  DdNode ** <b>f</b>, <i>IN: array of DD roots to be stored</i>
  char ** <b>rootnames</b>, <i>IN: array of root names (or NULL)</i>
  char ** <b>varnames</b>, <i>IN: array of variable names (or NULL)</i>
  int * <b>auxids</b>, <i>IN: array of converted var IDs</i>
  int  <b>mode</b>, <i>IN: storing mode selector</i>
  Dddmp_VarInfoType  <b>varinfo</b>, <i>IN: extra info for variables in text mode</i>
  char * <b>fname</b>, <i>IN: File name</i>
  FILE * <b>fp</b> <i>IN: File pointer to the store file</i>
)
</pre>
<dd> Dumps the argument array of BDDs to file.
    Internal function doing inner steps of store for BDDs.
<p>

<dd> <b>Side Effects</b> Nodes are temporarily removed from the unique hash
    table. They are re-linked after the store operation in a 
    modified order.
<p>

<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddStore">Dddmp_cuddBddStore</a>
<a href="#Dddmp_cuddBddLoad">Dddmp_cuddBddLoad</a>
<a href="#Dddmp_cuddBddArrayLoad">Dddmp_cuddBddArrayLoad</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreBdd.c"TARGET="ABSTRACT"><CODE>dddmpStoreBdd.c</CODE></A>

<dt><pre>
<A NAME="DddmpCuddDdArrayLoadCnf"></A>
static int <I></I>
<B>DddmpCuddDdArrayLoadCnf</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  Dddmp_RootMatchType  <b>rootmatchmode</b>, <i>IN: storing mode selector</i>
  char ** <b>rootmatchnames</b>, <i>IN: sorted names for loaded roots</i>
  Dddmp_VarMatchType  <b>varmatchmode</b>, <i>IN: storing mode selector</i>
  char ** <b>varmatchnames</b>, <i>IN: array of variable names, by ids</i>
  int * <b>varmatchauxids</b>, <i>IN: array of variable auxids, by ids</i>
  int * <b>varcomposeids</b>, <i>IN: array of new ids, by ids</i>
  int  <b>mode</b>, <i>IN: computation mode</i>
  char * <b>file</b>, <i>IN: file name</i>
  FILE * <b>fp</b>, <i>IN: file pointer</i>
  DdNode *** <b>rootsPtrPtr</b>, <i>OUT: array of BDD roots</i>
  int * <b>nRoots</b> <i>OUT: number of BDDs returned</i>
)
</pre>
<dd> Reads a dump file representing the argument BDDs in CNF
    format.
      IFF mode == 0 Return the Clauses without Conjunction
      IFF mode == 1 Return the sets of BDDs without Quantification
      IFF mode == 2 Return the sets of BDDs AFTER Existential Quantification
<p>

<dd> <b>Side Effects</b> A vector of pointers to DD nodes is allocated and freed.
<p>

<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddArrayLoad">Dddmp_cuddBddArrayLoad</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpLoadCnf.c"TARGET="ABSTRACT"><CODE>dddmpLoadCnf.c</CODE></A>

<dt><pre>
<A NAME="DddmpCuddDdArrayLoad"></A>
static int <I></I>
<B>DddmpCuddDdArrayLoad</B>(
  Dddmp_DecompType  <b>ddType</b>, <i>IN: Selects decomp type</i>
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  Dddmp_RootMatchType  <b>rootMatchMode</b>, <i>IN: storing mode selector</i>
  char ** <b>rootmatchnames</b>, <i>IN: sorted names for loaded roots</i>
  Dddmp_VarMatchType  <b>varMatchMode</b>, <i>IN: storing mode selector</i>
  char ** <b>varmatchnames</b>, <i>IN: array of variable names, by ids</i>
  int * <b>varmatchauxids</b>, <i>IN: array of variable auxids, by ids</i>
  int * <b>varcomposeids</b>, <i>IN: array of new ids, by ids</i>
  int  <b>mode</b>, <i>IN: requested input file format</i>
  char * <b>file</b>, <i>IN: file name</i>
  FILE * <b>fp</b>, <i>IN: file pointer</i>
  DdNode *** <b>pproots</b> <i>OUT: array BDD roots (by reference)</i>
)
</pre>
<dd> Reads a dump file representing the argument BDDs. The header is
    common to both text and binary mode. The node list is either 
    in text or binary format. A dynamic vector of DD pointers 
    is allocated to support conversion from DD indexes to pointers.
    Several criteria are supported for variable match between file
    and dd manager. Several changes/permutations/compositions are allowed
    for variables while loading DDs. Variable of the dd manager are allowed 
    to match with variables on file on ids, permids, varnames, 
    varauxids; also direct composition between ids and 
    composeids is supported. More in detail:
    <ol>
    <li> varMatchMode=DDDMP_VAR_MATCHIDS <p>
    allows the loading of a DD keeping variable IDs unchanged
    (regardless of the variable ordering of the reading manager); this
    is useful, for example, when swapping DDs to file and restoring them
    later from file, after possible variable reordering activations.
    
    <li> varMatchMode=DDDMP_VAR_MATCHPERMIDS <p>
    is used to allow variable match according to the position in the ordering.
    
    <li> varMatchMode=DDDMP_VAR_MATCHNAMES <p>
    requires a non NULL varmatchnames parameter; this is a vector of
    strings in one-to-one correspondence with variable IDs of the
    reading manager. Variables in the DD file read are matched with
    manager variables according to their name (a non NULL varnames
    parameter was required while storing the DD file).
    
    <li> varMatchMode=DDDMP_VAR_MATCHIDS <p>
    has a meaning similar to DDDMP_VAR_MATCHNAMES, but integer auxiliary
    IDs are used instead of strings; the additional non NULL
    varmatchauxids parameter is needed.
    
    <li> varMatchMode=DDDMP_VAR_COMPOSEIDS <p>
    uses the additional varcomposeids parameter is used as array of
    variable ids to be composed with ids stored in file.
    </ol>
    
    In the present implementation, the array varnames (3), varauxids (4)
    and composeids (5) need to have one entry for each variable in the 
    DD manager (NULL pointers are allowed for unused variables
    in varnames). Hence variables need to be already present in the 
    manager. All arrays are sorted according to IDs.
<p>

<dd> <b>Side Effects</b> A vector of pointers to DD nodes is allocated and freed.
<p>

<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddArrayStore">Dddmp_cuddBddArrayStore</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpLoad.c"TARGET="ABSTRACT"><CODE>dddmpLoad.c</CODE></A>

<dt><pre>
<A NAME="DddmpCuddDdArrayStoreBdd"></A>
int <I></I>
<B>DddmpCuddDdArrayStoreBdd</B>(
  Dddmp_DecompType  <b>ddType</b>, <i>IN: Selects the decomp type: BDD or ADD</i>
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  char * <b>ddname</b>, <i>IN: DD name (or NULL)</i>
  int  <b>nRoots</b>, <i>IN: number of output BDD roots to be stored</i>
  DdNode ** <b>f</b>, <i>IN: array of DD roots to be stored</i>
  char ** <b>rootnames</b>, <i>IN: array of root names (or NULL)</i>
  char ** <b>varnames</b>, <i>IN: array of variable names (or NULL)</i>
  int * <b>auxids</b>, <i>IN: array of converted var IDs</i>
  int  <b>mode</b>, <i>IN: storing mode selector</i>
  Dddmp_VarInfoType  <b>varinfo</b>, <i>IN: extra info for variables in text mode</i>
  char * <b>fname</b>, <i>IN: File name</i>
  FILE * <b>fp</b> <i>IN: File pointer to the store file</i>
)
</pre>
<dd> Dumps the argument array of BDDs/ADDs to file. Internal 
    function doing inner steps of store for BDDs and ADDs.
    ADD store is presently supported only with the text format.
<p>

<dd> <b>Side Effects</b> Nodes are temporarily removed from the unique hash
    table. They are re-linked after the store operation in a 
    modified order.
<p>

<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddStore">Dddmp_cuddBddStore</a>
<a href="#Dddmp_cuddBddLoad">Dddmp_cuddBddLoad</a>
<a href="#Dddmp_cuddBddArrayLoad">Dddmp_cuddBddArrayLoad</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreAdd.c"TARGET="ABSTRACT"><CODE>dddmpStoreAdd.c</CODE></A>

<dt><pre>
<A NAME="DddmpCuddDdArrayStoreBlifBody"></A>
static int <I></I>
<B>DddmpCuddDdArrayStoreBlifBody</B>(
  DdManager * <b>ddMgr</b>, <i>IN: Manager</i>
  int  <b>n</b>, <i>IN: Number of output nodes to be dumped</i>
  DdNode ** <b>f</b>, <i>IN: Array of output nodes to be dumped</i>
  char ** <b>inputNames</b>, <i>IN: Array of input names (or NULL)</i>
  char ** <b>outputNames</b>, <i>IN: Array of output names (or NULL)</i>
  FILE * <b>fp</b> <i>IN: Pointer to the dump file</i>
)
</pre>
<dd> Writes a blif body representing the argument BDDs as a
    network of multiplexers. One multiplexer is written for each BDD
    node. It returns 1 in case of success; 0 otherwise (e.g.,
    out-of-memory, file system full, or an ADD with constants different
    from 0 and 1).
    DddmpCuddDdArrayStoreBlif does not close the file: This is the
    caller responsibility.
    DddmpCuddDdArrayStoreBlif uses a minimal unique subset of
    the hexadecimal address of a node as name for it.  If the argument
    inputNames is non-null, it is assumed to hold the pointers to the names
    of the inputs. Similarly for outputNames. This function prints out only
    .names part.
<p>

<dd> <b>Side Effects</b> None
<p>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreMisc.c"TARGET="ABSTRACT"><CODE>dddmpStoreMisc.c</CODE></A>

<dt><pre>
<A NAME="DddmpCuddDdArrayStoreBlifStep"></A>
static int <I></I>
<B>DddmpCuddDdArrayStoreBlifStep</B>(
  DdManager * <b>ddMgr</b>, <i></i>
  DdNode * <b>f</b>, <i></i>
  FILE * <b>fp</b>, <i></i>
  st_table * <b>visited</b>, <i></i>
  char ** <b>names</b> <i></i>
)
</pre>
<dd> Performs the recursive step of DddmpCuddDdArrayStoreBlif.
    Traverses the BDD f and writes a multiplexer-network description to
    the file pointed by fp in blif format.
    f is assumed to be a regular pointer and DddmpCuddDdArrayStoreBlifStep
    guarantees this assumption in the recursive calls.
<p>

<dd> <b>Side Effects</b> None
<p>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreMisc.c"TARGET="ABSTRACT"><CODE>dddmpStoreMisc.c</CODE></A>

<dt><pre>
<A NAME="DddmpCuddDdArrayStoreBlif"></A>
static int <I></I>
<B>DddmpCuddDdArrayStoreBlif</B>(
  DdManager * <b>ddMgr</b>, <i>IN: Manager</i>
  int  <b>n</b>, <i>IN: Number of output nodes to be dumped</i>
  DdNode ** <b>f</b>, <i>IN: Array of output nodes to be dumped</i>
  char ** <b>inputNames</b>, <i>IN: Array of input names (or NULL)</i>
  char ** <b>outputNames</b>, <i>IN: Array of output names (or NULL)</i>
  char * <b>modelName</b>, <i>IN: Model name (or NULL)</i>
  FILE * <b>fp</b> <i>IN: Pointer to the dump file</i>
)
</pre>
<dd> Writes a blif file representing the argument BDDs as a
    network of multiplexers. One multiplexer is written for each BDD
    node. It returns 1 in case of success; 0 otherwise (e.g.,
    out-of-memory, file system full, or an ADD with constants different
    from 0 and 1).
    DddmpCuddDdArrayStoreBlif does not close the file: This is the
    caller responsibility.
    DddmpCuddDdArrayStoreBlif uses a minimal unique subset of
    the hexadecimal address of a node as name for it.  If the argument
    inames is non-null, it is assumed to hold the pointers to the names
    of the inputs. Similarly for outputNames.
    It prefixes the string "NODE" to each nome to have "regular" names
    for each elements.
<p>

<dd> <b>Side Effects</b> None
<p>

<dd> <b>See Also</b> <code><a href="#DddmpCuddDdArrayStoreBlifBody">DddmpCuddDdArrayStoreBlifBody</a>
<a href="#Cudd_DumpBlif">Cudd_DumpBlif</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreMisc.c"TARGET="ABSTRACT"><CODE>dddmpStoreMisc.c</CODE></A>

<dt><pre>
<A NAME="DddmpCuddDdArrayStorePrefixBody"></A>
static int <I></I>
<B>DddmpCuddDdArrayStorePrefixBody</B>(
  DdManager * <b>ddMgr</b>, <i>IN: Manager</i>
  int  <b>n</b>, <i>IN: Number of output nodes to be dumped</i>
  DdNode ** <b>f</b>, <i>IN: Array of output nodes to be dumped</i>
  char ** <b>inputNames</b>, <i>IN: Array of input names (or NULL)</i>
  char ** <b>outputNames</b>, <i>IN: Array of output names (or NULL)</i>
  FILE * <b>fp</b> <i>IN: Pointer to the dump file</i>
)
</pre>
<dd> One multiplexer is written for each BDD node.
    It returns 1 in case of success; 0 otherwise (e.g., out-of-memory, file
    system full, or an ADD with constants different from 0 and 1).
    It does not close the file: This is the caller responsibility.
    It uses a minimal unique subset of the hexadecimal address of a node as
    name for it.
    If the argument inputNames is non-null, it is assumed to hold the
    pointers to the names of the inputs. Similarly for outputNames.
    For each BDD node of function f, variable v, then child T, and else
    child E it stores:
    f = v * T + v' * E
    that is
    (OR f (AND v T) (AND (NOT v) E))
    If E is a complemented child this results in the following
    (OR f (AND v T) (AND (NOT v) (NOT E)))
<p>

<dd> <b>Side Effects</b> None
<p>

<dd> <b>See Also</b> <code><a href="#DddmpCuddDdArrayStoreBlif">DddmpCuddDdArrayStoreBlif</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreMisc.c"TARGET="ABSTRACT"><CODE>dddmpStoreMisc.c</CODE></A>

<dt><pre>
<A NAME="DddmpCuddDdArrayStorePrefixStep"></A>
static int <I></I>
<B>DddmpCuddDdArrayStorePrefixStep</B>(
  DdManager * <b>ddMgr</b>, <i></i>
  DdNode * <b>f</b>, <i></i>
  FILE * <b>fp</b>, <i></i>
  st_table * <b>visited</b>, <i></i>
  char ** <b>names</b> <i></i>
)
</pre>
<dd> Performs the recursive step of
    DddmpCuddDdArrayStorePrefixBody.
    Traverses the BDD f and writes a multiplexer-network description to the
    file pointed by fp.
    For each BDD node of function f, variable v, then child T, and else
    child E it stores:
    f = v * T + v' * E
    that is
    (OR f (AND v T) (AND (NOT v) E))
    If E is a complemented child this results in the following
    (OR f (AND v T) (AND (NOT v) (NOT E)))
    f is assumed to be a regular pointer and the function guarantees this
    assumption in the recursive calls.
<p>

<dd> <b>Side Effects</b> None
<p>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreMisc.c"TARGET="ABSTRACT"><CODE>dddmpStoreMisc.c</CODE></A>

<dt><pre>
<A NAME="DddmpCuddDdArrayStorePrefix"></A>
static int <I></I>
<B>DddmpCuddDdArrayStorePrefix</B>(
  DdManager * <b>ddMgr</b>, <i>IN: Manager</i>
  int  <b>n</b>, <i>IN: Number of output nodes to be dumped</i>
  DdNode ** <b>f</b>, <i>IN: Array of output nodes to be dumped</i>
  char ** <b>inputNames</b>, <i>IN: Array of input names (or NULL)</i>
  char ** <b>outputNames</b>, <i>IN: Array of output names (or NULL)</i>
  char * <b>modelName</b>, <i>IN: Model name (or NULL)</i>
  FILE * <b>fp</b> <i>IN: Pointer to the dump file</i>
)
</pre>
<dd> One multiplexer is written for each BDD node.
    It returns 1 in case of success; 0 otherwise (e.g., out-of-memory, file
    system full, or an ADD with constants different from 0 and 1).
    It does not close the file: This is the caller responsibility.
    It uses a minimal unique subset of the hexadecimal address of a node as
    name for it.
    If the argument inputNames is non-null, it is assumed to hold the
    pointers to the names of the inputs. Similarly for outputNames.
    For each BDD node of function f, variable v, then child T, and else
    child E it stores:
    f = v * T + v' * E
    that is
    (OR f (AND v T) (AND (NOT v) E))
    If E is a complemented child this results in the following
    (OR f (AND v T) (AND (NOT v) (NOT E)))
    Comments (COMMENT) are added at the beginning of the description to
    describe inputs and outputs of the design.
    A buffer (BUF) is add on the output to cope with complemented functions.
<p>

<dd> <b>Side Effects</b> None
<p>

<dd> <b>See Also</b> <code><a href="#DddmpCuddDdArrayStoreBlif">DddmpCuddDdArrayStoreBlif</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreMisc.c"TARGET="ABSTRACT"><CODE>dddmpStoreMisc.c</CODE></A>

<dt><pre>
<A NAME="DddmpCuddDdArrayStoreSmvBody"></A>
static int <I></I>
<B>DddmpCuddDdArrayStoreSmvBody</B>(
  DdManager * <b>ddMgr</b>, <i>IN: Manager</i>
  int  <b>n</b>, <i>IN: Number of output nodes to be dumped</i>
  DdNode ** <b>f</b>, <i>IN: Array of output nodes to be dumped</i>
  char ** <b>inputNames</b>, <i>IN: Array of input names (or NULL)</i>
  char ** <b>outputNames</b>, <i>IN: Array of output names (or NULL)</i>
  FILE * <b>fp</b> <i>IN: Pointer to the dump file</i>
)
</pre>
<dd> One multiplexer is written for each BDD node.
    It returns 1 in case of success; 0 otherwise (e.g., out-of-memory, file
    system full, or an ADD with constants different from 0 and 1).
    It does not close the file: This is the caller responsibility.
    It uses a minimal unique subset of the hexadecimal address of a node as
    name for it.
    If the argument inputNames is non-null, it is assumed to hold the
    pointers to the names of the inputs. Similarly for outputNames.
    For each BDD node of function f, variable v, then child T, and else
    child E it stores:
    f = v * T + v' * E
    that is
    (OR f (AND v T) (AND (NOT v) E))
    If E is a complemented child this results in the following
    (OR f (AND v T) (AND (NOT v) (NOT E)))
<p>

<dd> <b>Side Effects</b> None
<p>

<dd> <b>See Also</b> <code><a href="#DddmpCuddDdArrayStoreBlif">DddmpCuddDdArrayStoreBlif</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreMisc.c"TARGET="ABSTRACT"><CODE>dddmpStoreMisc.c</CODE></A>

<dt><pre>
<A NAME="DddmpCuddDdArrayStoreSmvStep"></A>
static int <I></I>
<B>DddmpCuddDdArrayStoreSmvStep</B>(
  DdManager * <b>ddMgr</b>, <i></i>
  DdNode * <b>f</b>, <i></i>
  FILE * <b>fp</b>, <i></i>
  st_table * <b>visited</b>, <i></i>
  char ** <b>names</b> <i></i>
)
</pre>
<dd> Performs the recursive step of
    DddmpCuddDdArrayStoreSmvBody.
    Traverses the BDD f and writes a multiplexer-network description to the
    file pointed by fp.
    For each BDD node of function f, variable v, then child T, and else
    child E it stores:
    f = v * T + v' * E
    that is
    (OR f (AND v T) (AND (NOT v) E))
    If E is a complemented child this results in the following
    (OR f (AND v T) (AND (NOT v) (NOT E)))
    f is assumed to be a regular pointer and the function guarantees this
    assumption in the recursive calls.
<p>

<dd> <b>Side Effects</b> None
<p>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreMisc.c"TARGET="ABSTRACT"><CODE>dddmpStoreMisc.c</CODE></A>

<dt><pre>
<A NAME="DddmpCuddDdArrayStoreSmv"></A>
static int <I></I>
<B>DddmpCuddDdArrayStoreSmv</B>(
  DdManager * <b>ddMgr</b>, <i>IN: Manager</i>
  int  <b>n</b>, <i>IN: Number of output nodes to be dumped</i>
  DdNode ** <b>f</b>, <i>IN: Array of output nodes to be dumped</i>
  char ** <b>inputNames</b>, <i>IN: Array of input names (or NULL)</i>
  char ** <b>outputNames</b>, <i>IN: Array of output names (or NULL)</i>
  char * <b>modelName</b>, <i>IN: Model name (or NULL)</i>
  FILE * <b>fp</b> <i>IN: Pointer to the dump file</i>
)
</pre>
<dd> One multiplexer is written for each BDD node.
    It returns 1 in case of success; 0 otherwise (e.g., out-of-memory, file
    system full, or an ADD with constants different from 0 and 1).
    It does not close the file: This is the caller responsibility.
    It uses a minimal unique subset of the hexadecimal address of a node as
    name for it.
    If the argument inputNames is non-null, it is assumed to hold the
    pointers to the names of the inputs. Similarly for outputNames.
    For each BDD node of function f, variable v, then child T, and else
    child E it stores:
    f = v * T + v' * E
    that is
    (OR f (AND v T) (AND (NOT v) E))
    If E is a complemented child this results in the following
    (OR f (AND v T) (AND (NOT v) (NOT E)))
    Comments (COMMENT) are added at the beginning of the description to
    describe inputs and outputs of the design.
    A buffer (BUF) is add on the output to cope with complemented functions.
<p>

<dd> <b>Side Effects</b> None
<p>

<dd> <b>See Also</b> <code><a href="#DddmpCuddDdArrayStoreBlif">DddmpCuddDdArrayStoreBlif</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreMisc.c"TARGET="ABSTRACT"><CODE>dddmpStoreMisc.c</CODE></A>

<dt><pre>
<A NAME="DddmpDdNodesCheckIncomingAndScanPath"></A>
static void <I></I>
<B>DddmpDdNodesCheckIncomingAndScanPath</B>(
  DdNode * <b>f</b>, <i>IN: BDD node to be numbered</i>
  int  <b>pathLengthCurrent</b>, <i>IN: Current Path Length</i>
  int  <b>edgeInTh</b>, <i>IN: Max # In-Edges, after a Insert Cut Point</i>
  int  <b>pathLengthTh</b> <i>IN: Max Path Length (after, Insert a Cut Point)</i>
)
</pre>
<dd> Number nodes recursively in post-order.
    The "visited" flag is used with the right polarity.
    The node is assigned to a new CNF variable only if it is a "shared"
    node (i.e. the number of its incoming edges is greater than 1).
<p>

<dd> <b>Side Effects</b> "visited" flags are set.
<p>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeCnf.c</CODE></A>

<dt><pre>
<A NAME="DddmpDdNodesCheckIncomingAndScanPath"></A>
static void <I></I>
<B>DddmpDdNodesCheckIncomingAndScanPath</B>(
  DdNode * <b>f</b>, <i>IN: BDD node to be numbered</i>
  int  <b>pathLengthCurrent</b>, <i>IN: Current Path Length</i>
  int  <b>edgeInTh</b>, <i>IN: Max # In-Edges, after a Insert Cut Point</i>
  int  <b>pathLengthTh</b> <i>IN: Max Path Length (after, Insert a Cut Point)</i>
)
</pre>
<dd> Number nodes recursively in post-order.
    The "visited" flag is used with the right polarity.
    The node is assigned to a new CNF variable only if it is a "shared"
    node (i.e. the number of its incoming edges is greater than 1).
<p>

<dd> <b>Side Effects</b> "visited" flags are set.
<p>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpNodeCnf.c</CODE></A>

<dt><pre>
<A NAME="DddmpDdNodesCountEdgesAndNumber"></A>
int <I></I>
<B>DddmpDdNodesCountEdgesAndNumber</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  DdNode ** <b>f</b>, <i>IN: Array of BDDs</i>
  int  <b>rootN</b>, <i>IN: Number of BDD roots in the array of BDDs</i>
  int  <b>edgeInTh</b>, <i>IN: Max # In-Edges, after a Insert Cut Point</i>
  int  <b>pathLengthTh</b>, <i>IN: Max Path Length (after, Insert a Cut Point)</i>
  int * <b>cnfIds</b>, <i>OUT: CNF identifiers for variables</i>
  int  <b>id</b> <i>OUT: Number of Temporary Variables Introduced</i>
)
</pre>
<dd> Removes nodes from unique table and numbers each node according
    to the number of its incoming BDD edges.
<p>

<dd> <b>Side Effects</b> Nodes are temporarily removed from unique table
<p>

<dd> <b>See Also</b> <code><a href="#RemoveFromUniqueRecurCnf()">RemoveFromUniqueRecurCnf()</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeCnf.c</CODE></A>

<dt><pre>
<A NAME="DddmpDdNodesCountEdgesAndNumber"></A>
int <I></I>
<B>DddmpDdNodesCountEdgesAndNumber</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  DdNode ** <b>f</b>, <i>IN: Array of BDDs</i>
  int  <b>rootN</b>, <i>IN: Number of BDD roots in the array of BDDs</i>
  int  <b>edgeInTh</b>, <i>IN: Max # In-Edges, after a Insert Cut Point</i>
  int  <b>pathLengthTh</b>, <i>IN: Max Path Length (after, Insert a Cut Point)</i>
  int * <b>cnfIds</b>, <i>OUT: CNF identifiers for variables</i>
  int  <b>id</b> <i>OUT: Number of Temporary Variables Introduced</i>
)
</pre>
<dd> Removes nodes from unique table and numbers each node according
    to the number of its incoming BDD edges.
<p>

<dd> <b>Side Effects</b> Nodes are temporarily removed from unique table
<p>

<dd> <b>See Also</b> <code><a href="#RemoveFromUniqueRecurCnf()">RemoveFromUniqueRecurCnf()</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpNodeCnf.c</CODE></A>

<dt><pre>
<A NAME="DddmpDdNodesCountEdgesRecur"></A>
static int <I></I>
<B>DddmpDdNodesCountEdgesRecur</B>(
  DdNode * <b>f</b> <i>IN: root of the BDD</i>
)
</pre>
<dd> Counts (recursively) the number of incoming edges for each 
    node of a BDD. This number is stored in the index field.
<p>

<dd> <b>Side Effects</b> "visited" flags remain untouched.
<p>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeCnf.c</CODE></A>

<dt><pre>
<A NAME="DddmpDdNodesCountEdgesRecur"></A>
static int <I></I>
<B>DddmpDdNodesCountEdgesRecur</B>(
  DdNode * <b>f</b> <i>IN: root of the BDD</i>
)
</pre>
<dd> Counts (recursively) the number of incoming edges for each 
    node of a BDD. This number is stored in the index field.
<p>

<dd> <b>Side Effects</b> "visited" flags remain untouched.
<p>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpNodeCnf.c</CODE></A>

<dt><pre>
<A NAME="DddmpDdNodesNumberEdgesRecur"></A>
static int <I></I>
<B>DddmpDdNodesNumberEdgesRecur</B>(
  DdNode * <b>f</b>, <i>IN: BDD node to be numbered</i>
  int * <b>cnfIds</b>, <i>IN: possible source for numbering</i>
  int  <b>id</b> <i>IN/OUT: possible source for numbering</i>
)
</pre>
<dd> Number nodes recursively in post-order.
    The "visited" flag is used with the inverse polarity.
    Numbering follows the subsequent strategy:
    * if the index = 0 it remains so
    * if the index >= 1 it gets enumerated.
      This implies that the node is assigned to a new CNF variable only if
      it is not a terminal node otherwise it is assigned the index of
      the BDD variable.
<p>

<dd> <b>Side Effects</b> "visited" flags are reset.
<p>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeCnf.c</CODE></A>

<dt><pre>
<A NAME="DddmpDdNodesNumberEdgesRecur"></A>
static int <I></I>
<B>DddmpDdNodesNumberEdgesRecur</B>(
  DdNode * <b>f</b>, <i>IN: BDD node to be numbered</i>
  int * <b>cnfIds</b>, <i>IN: possible source for numbering</i>
  int  <b>id</b> <i>IN/OUT: possible source for numbering</i>
)
</pre>
<dd> Number nodes recursively in post-order.
    The "visited" flag is used with the inverse polarity.
    Numbering follows the subsequent strategy:
    * if the index = 0 it remains so
    * if the index >= 1 it gets enumerated.
      This implies that the node is assigned to a new CNF variable only if
      it is not a terminal node otherwise it is assigned the index of
      the BDD variable.
<p>

<dd> <b>Side Effects</b> "visited" flags are reset.
<p>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpNodeCnf.c</CODE></A>

<dt><pre>
<A NAME="DddmpDdNodesResetCountRecur"></A>
static int <I></I>
<B>DddmpDdNodesResetCountRecur</B>(
  DdNode * <b>f</b> <i>IN: root of the BDD whose counters are reset</i>
)
</pre>
<dd> Resets counter and visited flag for ALL nodes of a BDD (it 
    recurs on the node children). The index field of the node is 
    used as counter.
<p>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeCnf.c</CODE></A>

<dt><pre>
<A NAME="DddmpDdNodesResetCountRecur"></A>
static int <I></I>
<B>DddmpDdNodesResetCountRecur</B>(
  DdNode * <b>f</b> <i>IN: root of the BDD whose counters are reset</i>
)
</pre>
<dd> Resets counter and visited flag for ALL nodes of a BDD (it 
    recurs on the node children). The index field of the node is 
    used as counter.
<p>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpNodeCnf.c</CODE></A>

<dt><pre>
<A NAME="DddmpFreeHeaderCnf"></A>
static void <I></I>
<B>DddmpFreeHeaderCnf</B>(
  Dddmp_Hdr_t * <b>Hdr</b> <i>IN: pointer to header</i>
)
</pre>
<dd> Frees the internal header structure by freeing all internal
    fields first.
<p>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpLoadCnf.c"TARGET="ABSTRACT"><CODE>dddmpLoadCnf.c</CODE></A>

<dt><pre>
<A NAME="DddmpFreeHeader"></A>
static void <I></I>
<B>DddmpFreeHeader</B>(
  Dddmp_Hdr_t * <b>Hdr</b> <i>IN: pointer to header</i>
)
</pre>
<dd> Frees the internal header structureby freeing all internal
    fields first.
<p>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpLoad.c"TARGET="ABSTRACT"><CODE>dddmpLoad.c</CODE></A>

<dt><pre>
<A NAME="DddmpIntArrayDup"></A>
int * <I></I>
<B>DddmpIntArrayDup</B>(
  int * <b>array</b>, <i>IN: array of ints to be duplicated</i>
  int  <b>n</b> <i>IN: size of the array</i>
)
</pre>
<dd> Allocates memory and copies source array
<p>

<dd> <b>Side Effects</b> None
<p>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpUtil.c"TARGET="ABSTRACT"><CODE>dddmpUtil.c</CODE></A>

<dt><pre>
<A NAME="DddmpIntArrayRead"></A>
int * <I></I>
<B>DddmpIntArrayRead</B>(
  FILE * <b>fp</b>, <i>IN: input file</i>
  int  <b>n</b> <i>IN: size of the array</i>
)
</pre>
<dd> Allocates memory and inputs source array
<p>

<dd> <b>Side Effects</b> None
<p>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpUtil.c"TARGET="ABSTRACT"><CODE>dddmpUtil.c</CODE></A>

<dt><pre>
<A NAME="DddmpIntArrayWrite"></A>
int <I></I>
<B>DddmpIntArrayWrite</B>(
  FILE * <b>fp</b>, <i>IN: output file</i>
  int * <b>array</b>, <i>IN: array of ints</i>
  int  <b>n</b> <i>IN: size of the array</i>
)
</pre>
<dd> Outputs an array of ints to a specified file
<p>

<dd> <b>Side Effects</b> None
<p>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpUtil.c"TARGET="ABSTRACT"><CODE>dddmpUtil.c</CODE></A>

<dt><pre>
<A NAME="DddmpNumberAddNodes"></A>
int <I></I>
<B>DddmpNumberAddNodes</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  DdNode ** <b>f</b>, <i>IN: array of BDDs</i>
  int  <b>n</b> <i>IN: number of BDD roots in the array of BDDs</i>
)
</pre>
<dd> Node numbering is required to convert pointers to integers.
    Since nodes are removed from unique table, no new nodes should 
    be generated before re-inserting nodes in the unique table
    (DddmpUnnumberDdNodes()).
<p>

<dd> <b>Side Effects</b> Nodes are temporarily removed from unique table
<p>

<dd> <b>See Also</b> <code><a href="#RemoveFromUniqueRecurAdd">RemoveFromUniqueRecurAdd</a>
()
<a href="#NumberNodeRecurAdd">NumberNodeRecurAdd</a>
()
<a href="#DddmpUnnumberDdNodesAdd">DddmpUnnumberDdNodesAdd</a>
()
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeAdd.c"TARGET="ABSTRACT"><CODE>dddmpNodeAdd.c</CODE></A>

<dt><pre>
<A NAME="DddmpNumberBddNodes"></A>
int <I></I>
<B>DddmpNumberBddNodes</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  DdNode ** <b>f</b>, <i>IN: array of BDDs</i>
  int  <b>n</b> <i>IN: number of BDD roots in the array of BDDs</i>
)
</pre>
<dd> Node numbering is required to convert pointers to integers.
    Since nodes are removed from unique table, no new nodes should 
    be generated before re-inserting nodes in the unique table
    (DddmpUnnumberBddNodes ()).
<p>

<dd> <b>Side Effects</b> Nodes are temporarily removed from unique table
<p>

<dd> <b>See Also</b> <code><a href="#RemoveFromUniqueRecur()">RemoveFromUniqueRecur()</a>
<a href="#NumberNodeRecur()">NumberNodeRecur()</a>
<a href="#DddmpUnnumberBddNodes">DddmpUnnumberBddNodes</a>
()
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeBdd.c"TARGET="ABSTRACT"><CODE>dddmpNodeBdd.c</CODE></A>

<dt><pre>
<A NAME="DddmpNumberDdNodesCnf"></A>
int <I></I>
<B>DddmpNumberDdNodesCnf</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  DdNode ** <b>f</b>, <i>IN: array of BDDs</i>
  int  <b>rootN</b>, <i>IN: number of BDD roots in the array of BDDs</i>
  int * <b>cnfIds</b>, <i>OUT: CNF identifiers for variables</i>
  int  <b>id</b> <i>OUT: number of Temporary Variables Introduced</i>
)
</pre>
<dd> Node numbering is required to convert pointers to integers.
    Since nodes are removed from unique table, no new nodes should 
    be generated before re-inserting nodes in the unique table
    (DddmpUnnumberDdNodesCnf()).
<p>

<dd> <b>Side Effects</b> Nodes are temporarily removed from unique table
<p>

<dd> <b>See Also</b> <code><a href="#RemoveFromUniqueRecurCnf()">RemoveFromUniqueRecurCnf()</a>
<a href="#NumberNodeRecurCnf()">NumberNodeRecurCnf()</a>
<a href="#DddmpUnnumberDdNodesCnf()">DddmpUnnumberDdNodesCnf()</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeCnf.c</CODE></A>

<dt><pre>
<A NAME="DddmpNumberDdNodesCnf"></A>
int <I></I>
<B>DddmpNumberDdNodesCnf</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  DdNode ** <b>f</b>, <i>IN: array of BDDs</i>
  int  <b>rootN</b>, <i>IN: number of BDD roots in the array of BDDs</i>
  int * <b>cnfIds</b>, <i>OUT: CNF identifiers for variables</i>
  int  <b>id</b> <i>OUT: number of Temporary Variables Introduced</i>
)
</pre>
<dd> Node numbering is required to convert pointers to integers.
    Since nodes are removed from unique table, no new nodes should 
    be generated before re-inserting nodes in the unique table
    (DddmpUnnumberDdNodesCnf()).
<p>

<dd> <b>Side Effects</b> Nodes are temporarily removed from unique table
<p>

<dd> <b>See Also</b> <code><a href="#RemoveFromUniqueRecurCnf()">RemoveFromUniqueRecurCnf()</a>
<a href="#NumberNodeRecurCnf()">NumberNodeRecurCnf()</a>
<a href="#DddmpUnnumberDdNodesCnf()">DddmpUnnumberDdNodesCnf()</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpNodeCnf.c</CODE></A>

<dt><pre>
<A NAME="DddmpNumberDdNodes"></A>
int <I></I>
<B>DddmpNumberDdNodes</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  DdNode ** <b>f</b>, <i>IN: array of BDDs</i>
  int  <b>n</b> <i>IN: number of BDD roots in the array of BDDs</i>
)
</pre>
<dd> Node numbering is required to convert pointers to integers.
    Since nodes are removed from unique table, no new nodes should 
    be generated before re-inserting nodes in the unique table
    (DddmpUnnumberDdNodes()).
<p>

<dd> <b>Side Effects</b> Nodes are temporarily removed from unique table
<p>

<dd> <b>See Also</b> <code><a href="#RemoveFromUniqueRecur()">RemoveFromUniqueRecur()</a>
<a href="#NumberNodeRecur()">NumberNodeRecur()</a>
<a href="#DddmpUnnumberDdNodes()">DddmpUnnumberDdNodes()</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeBdd.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeBdd.c</CODE></A>

<dt><pre>
<A NAME="DddmpPrintBddAndNextRecur"></A>
static int <I></I>
<B>DddmpPrintBddAndNextRecur</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  DdNode * <b>f</b> <i>IN: root of the BDD to be displayed</i>
)
</pre>
<dd> Prints debug info for a BDD on the screen. It recurs on 
    node's children.
<p>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeCnf.c</CODE></A>

<dt><pre>
<A NAME="DddmpPrintBddAndNextRecur"></A>
static int <I></I>
<B>DddmpPrintBddAndNextRecur</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  DdNode * <b>f</b> <i>IN: root of the BDD to be displayed</i>
)
</pre>
<dd> Prints debug info for a BDD on the screen. It recurs on 
    node's children.
<p>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpNodeCnf.c</CODE></A>

<dt><pre>
<A NAME="DddmpPrintBddAndNext"></A>
int <I></I>
<B>DddmpPrintBddAndNext</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  DdNode ** <b>f</b>, <i>IN: Array of BDDs to be displayed</i>
  int  <b>rootN</b> <i>IN: Number of BDD roots in the array of BDDs</i>
)
</pre>
<dd> Prints debug information for an array of BDDs on the screen
<p>

<dd> <b>Side Effects</b> None
<p>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeCnf.c</CODE></A>

<dt><pre>
<A NAME="DddmpPrintBddAndNext"></A>
int <I></I>
<B>DddmpPrintBddAndNext</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  DdNode ** <b>f</b>, <i>IN: Array of BDDs to be displayed</i>
  int  <b>rootN</b> <i>IN: Number of BDD roots in the array of BDDs</i>
)
</pre>
<dd> Prints debug information for an array of BDDs on the screen
<p>

<dd> <b>Side Effects</b> None
<p>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpNodeCnf.c</CODE></A>

<dt><pre>
<A NAME="DddmpReadCnfClauses"></A>
static int <I></I>
<B>DddmpReadCnfClauses</B>(
  Dddmp_Hdr_t * <b>Hdr</b>, <i>IN: file header</i>
  int *** <b>cnfTable</b>, <i>OUT: CNF table for clauses</i>
  FILE * <b>fp</b> <i>IN: source file</i>
)
</pre>
<dd> Read the CNF clauses from the file in the standard DIMACS
    format. Store all the clauses in an internal structure for 
    future transformation into BDDs.
<p>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpLoadCnf.c"TARGET="ABSTRACT"><CODE>dddmpLoadCnf.c</CODE></A>

<dt><pre>
<A NAME="DddmpReadCode"></A>
int <I></I>
<B>DddmpReadCode</B>(
  FILE * <b>fp</b>, <i>IN: file where to read the code</i>
  struct binary_dd_code * <b>pcode</b> <i>OUT: the read code</i>
)
</pre>
<dd> Reads a 1 byte node code. See DddmpWriteCode()
    for code description.
<p>

<dd> <b>Side Effects</b> None
<p>

<dd> <b>See Also</b> <code><a href="#DddmpWriteCode()">DddmpWriteCode()</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpBinary.c"TARGET="ABSTRACT"><CODE>dddmpBinary.c</CODE></A>

<dt><pre>
<A NAME="DddmpReadInt"></A>
int <I></I>
<B>DddmpReadInt</B>(
  FILE * <b>fp</b>, <i>IN: file where to read the integer</i>
  int * <b>pid</b> <i>OUT: the read integer</i>
)
</pre>
<dd> Reads an integer coded on a sequence of bytes. See
    DddmpWriteInt() for format.
<p>

<dd> <b>Side Effects</b> None
<p>

<dd> <b>See Also</b> <code><a href="#DddmpWriteInt()">DddmpWriteInt()</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpBinary.c"TARGET="ABSTRACT"><CODE>dddmpBinary.c</CODE></A>

<dt><pre>
<A NAME="DddmpReadNodeIndexAdd"></A>
int <I></I>
<B>DddmpReadNodeIndexAdd</B>(
  DdNode * <b>f</b> <i>IN: BDD node</i>
)
</pre>
<dd> Reads the index of a node. LSB is skipped (used as visited
    flag).
<p>

<dd> <b>Side Effects</b> None
<p>

<dd> <b>See Also</b> <code><a href="#DddmpWriteNodeIndexAdd">DddmpWriteNodeIndexAdd</a>
()
<a href="#DddmpSetVisitedAdd">DddmpSetVisitedAdd</a>
()
<a href="#DddmpVisitedAdd">DddmpVisitedAdd</a>
()
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeAdd.c"TARGET="ABSTRACT"><CODE>dddmpNodeAdd.c</CODE></A>

<dt><pre>
<A NAME="DddmpReadNodeIndexBdd"></A>
int <I></I>
<B>DddmpReadNodeIndexBdd</B>(
  DdNode * <b>f</b> <i>IN: BDD node</i>
)
</pre>
<dd> Reads the index of a node. LSB is skipped (used as visited
    flag).
<p>

<dd> <b>Side Effects</b> None
<p>

<dd> <b>See Also</b> <code><a href="#DddmpWriteNodeIndexBdd">DddmpWriteNodeIndexBdd</a>
()
<a href="#DddmpSetVisitedBdd">DddmpSetVisitedBdd</a>
()
<a href="#DddmpVisitedBdd">DddmpVisitedBdd</a>
()
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeBdd.c"TARGET="ABSTRACT"><CODE>dddmpNodeBdd.c</CODE></A>

<dt><pre>
<A NAME="DddmpReadNodeIndexCnf"></A>
int <I></I>
<B>DddmpReadNodeIndexCnf</B>(
  DdNode * <b>f</b> <i>IN: BDD node</i>
)
</pre>
<dd> Reads the index of a node. LSB is skipped (used as visited
    flag).
<p>

<dd> <b>Side Effects</b> None
<p>

<dd> <b>See Also</b> <code><a href="#DddmpWriteNodeIndexCnf()">DddmpWriteNodeIndexCnf()</a>
<a href="#DddmpSetVisitedCnf">DddmpSetVisitedCnf</a>
()
<a href="#DddmpVisitedCnf">DddmpVisitedCnf</a>
()
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpNodeCnf.c</CODE></A>

<dt><pre>
<A NAME="DddmpReadNodeIndexCnf"></A>
static int <I></I>
<B>DddmpReadNodeIndexCnf</B>(
  DdNode * <b>f</b> <i>IN: BDD node</i>
)
</pre>
<dd> Reads the index of a node. LSB is skipped (used as visited
                flag).
<p>

<dd> <b>Side Effects</b> None
<p>

<dd> <b>See Also</b> <code><a href="#DddmpWriteNodeIndexCnf()">DddmpWriteNodeIndexCnf()</a>
<a href="#DddmpSetVisitedCnf">DddmpSetVisitedCnf</a>
()
<a href="#DddmpVisitedCnf">DddmpVisitedCnf</a>
()
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeCnf.c</CODE></A>

<dt><pre>
<A NAME="DddmpReadNodeIndex"></A>
int <I></I>
<B>DddmpReadNodeIndex</B>(
  DdNode * <b>f</b> <i>IN: BDD node</i>
)
</pre>
<dd> Reads the index of a node. LSB is skipped (used as visited
    flag).
<p>

<dd> <b>Side Effects</b> None
<p>

<dd> <b>See Also</b> <code><a href="#DddmpWriteNodeIndex()">DddmpWriteNodeIndex()</a>
<a href="#DddmpSetVisited">DddmpSetVisited</a>
()
<a href="#DddmpVisited">DddmpVisited</a>
()
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeBdd.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeBdd.c</CODE></A>

<dt><pre>
<A NAME="DddmpSetVisitedAdd"></A>
void <I></I>
<B>DddmpSetVisitedAdd</B>(
  DdNode * <b>f</b> <i>IN: BDD node to be marked (as visited)</i>
)
</pre>
<dd> Marks a node as visited
<p>

<dd> <b>Side Effects</b> None
<p>

<dd> <b>See Also</b> <code><a href="#DddmpVisitedAdd">DddmpVisitedAdd</a>
()
<a href="#DddmpClearVisitedAdd">DddmpClearVisitedAdd</a>
()
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeAdd.c"TARGET="ABSTRACT"><CODE>dddmpNodeAdd.c</CODE></A>

<dt><pre>
<A NAME="DddmpSetVisitedBdd"></A>
void <I></I>
<B>DddmpSetVisitedBdd</B>(
  DdNode * <b>f</b> <i>IN: BDD node to be marked (as visited)</i>
)
</pre>
<dd> Marks a node as visited
<p>

<dd> <b>Side Effects</b> None
<p>

<dd> <b>See Also</b> <code><a href="#DddmpVisitedBdd">DddmpVisitedBdd</a>
()
<a href="#DddmpClearVisitedBdd">DddmpClearVisitedBdd</a>
()
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeBdd.c"TARGET="ABSTRACT"><CODE>dddmpNodeBdd.c</CODE></A>

<dt><pre>
<A NAME="DddmpSetVisitedCnf"></A>
static void <I></I>
<B>DddmpSetVisitedCnf</B>(
  DdNode * <b>f</b> <i>IN: BDD node to be marked (as visited)</i>
)
</pre>
<dd> Marks a node as visited
<p>

<dd> <b>Side Effects</b> None
<p>

<dd> <b>See Also</b> <code><a href="#DddmpVisitedCnf">DddmpVisitedCnf</a>
()
<a href="#DddmpClearVisitedCnf">DddmpClearVisitedCnf</a>
()
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeCnf.c</CODE></A>

<dt><pre>
<A NAME="DddmpSetVisitedCnf"></A>
void <I></I>
<B>DddmpSetVisitedCnf</B>(
  DdNode * <b>f</b> <i>IN: BDD node to be marked (as visited)</i>
)
</pre>
<dd> Marks a node as visited
<p>

<dd> <b>Side Effects</b> None
<p>

<dd> <b>See Also</b> <code><a href="#DddmpVisitedCnf">DddmpVisitedCnf</a>
()
<a href="#DddmpClearVisitedCnf">DddmpClearVisitedCnf</a>
()
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpNodeCnf.c</CODE></A>

<dt><pre>
<A NAME="DddmpSetVisited"></A>
void <I></I>
<B>DddmpSetVisited</B>(
  DdNode * <b>f</b> <i>IN: BDD node to be marked (as visited)</i>
)
</pre>
<dd> Marks a node as visited
<p>

<dd> <b>Side Effects</b> None
<p>

<dd> <b>See Also</b> <code><a href="#DddmpVisited">DddmpVisited</a>
()
<a href="#DddmpClearVisited">DddmpClearVisited</a>
()
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeBdd.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeBdd.c</CODE></A>

<dt><pre>
<A NAME="DddmpStrArrayDup"></A>
char ** <I></I>
<B>DddmpStrArrayDup</B>(
  char ** <b>array</b>, <i>IN: array of strings to be duplicated</i>
  int  <b>n</b> <i>IN: size of the array</i>
)
</pre>
<dd> Allocates memory and copies source array
<p>

<dd> <b>Side Effects</b> None
<p>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpUtil.c"TARGET="ABSTRACT"><CODE>dddmpUtil.c</CODE></A>

<dt><pre>
<A NAME="DddmpStrArrayFree"></A>
void <I></I>
<B>DddmpStrArrayFree</B>(
  char ** <b>array</b>, <i>IN: array of strings</i>
  int  <b>n</b> <i>IN: size of the array</i>
)
</pre>
<dd> Frees memory for strings and the array of pointers
<p>

<dd> <b>Side Effects</b> None
<p>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpUtil.c"TARGET="ABSTRACT"><CODE>dddmpUtil.c</CODE></A>

<dt><pre>
<A NAME="DddmpStrArrayRead"></A>
char ** <I></I>
<B>DddmpStrArrayRead</B>(
  FILE * <b>fp</b>, <i>IN: input file</i>
  int  <b>n</b> <i>IN: size of the array</i>
)
</pre>
<dd> Allocates memory and inputs source array
<p>

<dd> <b>Side Effects</b> None
<p>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpUtil.c"TARGET="ABSTRACT"><CODE>dddmpUtil.c</CODE></A>

<dt><pre>
<A NAME="DddmpStrArrayWrite"></A>
int <I></I>
<B>DddmpStrArrayWrite</B>(
  FILE * <b>fp</b>, <i>IN: output file</i>
  char ** <b>array</b>, <i>IN: array of strings</i>
  int  <b>n</b> <i>IN: size of the array</i>
)
</pre>
<dd> Outputs an array of strings to a specified file
<p>

<dd> <b>Side Effects</b> None
<p>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpUtil.c"TARGET="ABSTRACT"><CODE>dddmpUtil.c</CODE></A>

<dt><pre>
<A NAME="DddmpStrDup"></A>
char * <I></I>
<B>DddmpStrDup</B>(
  char * <b>str</b> <i>IN: string to be duplicated</i>
)
</pre>
<dd> Allocates memory and copies source string
<p>

<dd> <b>Side Effects</b> None
<p>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpUtil.c"TARGET="ABSTRACT"><CODE>dddmpUtil.c</CODE></A>

<dt><pre>
<A NAME="DddmpUnnumberAddNodes"></A>
void <I></I>
<B>DddmpUnnumberAddNodes</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  DdNode ** <b>f</b>, <i>IN: array of BDDs</i>
  int  <b>n</b> <i>IN: number of BDD roots in the array of BDDs</i>
)
</pre>
<dd> Node indexes are no more needed. Nodes are re-linked in the
    unique table.
<p>

<dd> <b>Side Effects</b> None
<p>

<dd> <b>See Also</b> <code><a href="#DddmpNumberDdNodeAdd">DddmpNumberDdNodeAdd</a>
()
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeAdd.c"TARGET="ABSTRACT"><CODE>dddmpNodeAdd.c</CODE></A>

<dt><pre>
<A NAME="DddmpUnnumberBddNodes"></A>
void <I></I>
<B>DddmpUnnumberBddNodes</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  DdNode ** <b>f</b>, <i>IN: array of BDDs</i>
  int  <b>n</b> <i>IN: number of BDD roots in the array of BDDs</i>
)
</pre>
<dd> Node indexes are no more needed. Nodes are re-linked in the
    unique table.
<p>

<dd> <b>Side Effects</b> None
<p>

<dd> <b>See Also</b> <code><a href="#DddmpNumberBddNode">DddmpNumberBddNode</a>
()
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeBdd.c"TARGET="ABSTRACT"><CODE>dddmpNodeBdd.c</CODE></A>

<dt><pre>
<A NAME="DddmpUnnumberDdNodesCnf"></A>
void <I></I>
<B>DddmpUnnumberDdNodesCnf</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  DdNode ** <b>f</b>, <i>IN: array of BDDs</i>
  int  <b>rootN</b> <i>IN: number of BDD roots in the array of BDDs</i>
)
</pre>
<dd> Node indexes are no more needed. Nodes are re-linked in the
    unique table.
<p>

<dd> <b>Side Effects</b> None
<p>

<dd> <b>See Also</b> <code><a href="#DddmpNumberDdNode()">DddmpNumberDdNode()</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeCnf.c</CODE></A>

<dt><pre>
<A NAME="DddmpUnnumberDdNodesCnf"></A>
void <I></I>
<B>DddmpUnnumberDdNodesCnf</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  DdNode ** <b>f</b>, <i>IN: array of BDDs</i>
  int  <b>rootN</b> <i>IN: number of BDD roots in the array of BDDs</i>
)
</pre>
<dd> Node indexes are no more needed. Nodes are re-linked in the
    unique table.
<p>

<dd> <b>Side Effects</b> None
<p>

<dd> <b>See Also</b> <code><a href="#DddmpNumberDdNode()">DddmpNumberDdNode()</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpNodeCnf.c</CODE></A>

<dt><pre>
<A NAME="DddmpUnnumberDdNodes"></A>
void <I></I>
<B>DddmpUnnumberDdNodes</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  DdNode ** <b>f</b>, <i>IN: array of BDDs</i>
  int  <b>n</b> <i>IN: number of BDD roots in the array of BDDs</i>
)
</pre>
<dd> Node indexes are no more needed. Nodes are re-linked in the
    unique table.
<p>

<dd> <b>Side Effects</b> None
<p>

<dd> <b>See Also</b> <code><a href="#DddmpNumberDdNode()">DddmpNumberDdNode()</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeBdd.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeBdd.c</CODE></A>

<dt><pre>
<A NAME="DddmpVisitedAdd"></A>
int <I></I>
<B>DddmpVisitedAdd</B>(
  DdNode * <b>f</b> <i>IN: BDD node to be tested</i>
)
</pre>
<dd> Returns true if node is visited
<p>

<dd> <b>Side Effects</b> None
<p>

<dd> <b>See Also</b> <code><a href="#DddmpSetVisitedAdd">DddmpSetVisitedAdd</a>
()
<a href="#DddmpClearVisitedAdd">DddmpClearVisitedAdd</a>
()
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeAdd.c"TARGET="ABSTRACT"><CODE>dddmpNodeAdd.c</CODE></A>

<dt><pre>
<A NAME="DddmpVisitedBdd"></A>
int <I></I>
<B>DddmpVisitedBdd</B>(
  DdNode * <b>f</b> <i>IN: BDD node to be tested</i>
)
</pre>
<dd> Returns true if node is visited
<p>

<dd> <b>Side Effects</b> None
<p>

<dd> <b>See Also</b> <code><a href="#DddmpSetVisitedBdd">DddmpSetVisitedBdd</a>
()
<a href="#DddmpClearVisitedBdd">DddmpClearVisitedBdd</a>
()
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeBdd.c"TARGET="ABSTRACT"><CODE>dddmpNodeBdd.c</CODE></A>

<dt><pre>
<A NAME="DddmpVisitedCnf"></A>
int <I></I>
<B>DddmpVisitedCnf</B>(
  DdNode * <b>f</b> <i>IN: BDD node to be tested</i>
)
</pre>
<dd> Returns true if node is visited
<p>

<dd> <b>Side Effects</b> None
<p>

<dd> <b>See Also</b> <code><a href="#DddmpSetVisitedCnf">DddmpSetVisitedCnf</a>
()
<a href="#DddmpClearVisitedCnf">DddmpClearVisitedCnf</a>
()
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpNodeCnf.c</CODE></A>

<dt><pre>
<A NAME="DddmpVisitedCnf"></A>
static int <I></I>
<B>DddmpVisitedCnf</B>(
  DdNode * <b>f</b> <i>IN: BDD node to be tested</i>
)
</pre>
<dd> Returns true if node is visited
<p>

<dd> <b>Side Effects</b> None
<p>

<dd> <b>See Also</b> <code><a href="#DddmpSetVisitedCnf">DddmpSetVisitedCnf</a>
()
<a href="#DddmpClearVisitedCnf">DddmpClearVisitedCnf</a>
()
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeCnf.c</CODE></A>

<dt><pre>
<A NAME="DddmpVisited"></A>
int <I></I>
<B>DddmpVisited</B>(
  DdNode * <b>f</b> <i>IN: BDD node to be tested</i>
)
</pre>
<dd> Returns true if node is visited
<p>

<dd> <b>Side Effects</b> None
<p>

<dd> <b>See Also</b> <code><a href="#DddmpSetVisited">DddmpSetVisited</a>
()
<a href="#DddmpClearVisited">DddmpClearVisited</a>
()
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeBdd.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeBdd.c</CODE></A>

<dt><pre>
<A NAME="DddmpWriteCode"></A>
int <I></I>
<B>DddmpWriteCode</B>(
  FILE * <b>fp</b>, <i>IN: file where to write the code</i>
  struct binary_dd_code  <b>code</b> <i>IN: the code to be written</i>
)
</pre>
<dd> outputs a 1 byte node code using the following format:
     <pre>
     Unused      : 1 bit;
     V           : 2 bits;     (variable code)
     T           : 2 bits;     (Then code)
     Ecompl      : 1 bit;      (Else complemented)
     E           : 2 bits;     (Else code)
    </pre>
    Ecompl is set with complemented edges.
<p>

<dd> <b>Side Effects</b> None
<p>

<dd> <b>See Also</b> <code><a href="#DddmpReadCode()">DddmpReadCode()</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpBinary.c"TARGET="ABSTRACT"><CODE>dddmpBinary.c</CODE></A>

<dt><pre>
<A NAME="DddmpWriteInt"></A>
int <I></I>
<B>DddmpWriteInt</B>(
  FILE * <b>fp</b>, <i>IN: file where to write the integer</i>
  int  <b>id</b> <i>IN: integer to be written</i>
)
</pre>
<dd> Writes an integer as a sequence of bytes (MSByte first).
    For each byte 7 bits are used for data and one (LSBit) as link 
    with a further byte (LSB = 1 means one more byte).
<p>

<dd> <b>Side Effects</b> None
<p>

<dd> <b>See Also</b> <code><a href="#DddmpReadInt()">DddmpReadInt()</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpBinary.c"TARGET="ABSTRACT"><CODE>dddmpBinary.c</CODE></A>

<dt><pre>
<A NAME="DddmpWriteNodeIndexAdd"></A>
void <I></I>
<B>DddmpWriteNodeIndexAdd</B>(
  DdNode * <b>f</b>, <i>IN: BDD node</i>
  int  <b>id</b> <i>IN: index to be written</i>
)
</pre>
<dd> The index of the node is written in the "next" field of
    a DdNode struct. LSB is not used (set to 0). It is used as 
    "visited" flag in DD traversals.
<p>

<dd> <b>Side Effects</b> None
<p>

<dd> <b>See Also</b> <code><a href="#DddmpReadNodeIndexAdd">DddmpReadNodeIndexAdd</a>
()
<a href="#DddmpSetVisitedAdd">DddmpSetVisitedAdd</a>
()
<a href="#DddmpVisitedAdd">DddmpVisitedAdd</a>
()
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeAdd.c"TARGET="ABSTRACT"><CODE>dddmpNodeAdd.c</CODE></A>

<dt><pre>
<A NAME="DddmpWriteNodeIndexBdd"></A>
void <I></I>
<B>DddmpWriteNodeIndexBdd</B>(
  DdNode * <b>f</b>, <i>IN: BDD node</i>
  int  <b>id</b> <i>IN: index to be written</i>
)
</pre>
<dd> The index of the node is written in the "next" field of
    a DdNode struct. LSB is not used (set to 0). It is used as 
    "visited" flag in DD traversals.
<p>

<dd> <b>Side Effects</b> None
<p>

<dd> <b>See Also</b> <code><a href="#DddmpReadNodeIndexBdd()">DddmpReadNodeIndexBdd()</a>
<a href="#DddmpSetVisitedBdd">DddmpSetVisitedBdd</a>
()
<a href="#DddmpVisitedBdd">DddmpVisitedBdd</a>
()
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeBdd.c"TARGET="ABSTRACT"><CODE>dddmpNodeBdd.c</CODE></A>

<dt><pre>
<A NAME="DddmpWriteNodeIndexCnfBis"></A>
int <I></I>
<B>DddmpWriteNodeIndexCnfBis</B>(
  DdNode * <b>f</b>, <i>IN: BDD node</i>
  int  <b>id</b> <i>IN: index to be written</i>
)
</pre>
<dd> The index of the node is written in the "next" field of
    a DdNode struct. LSB is not used (set to 0). It is used as 
    "visited" flag in DD traversals.
<p>

<dd> <b>Side Effects</b> None
<p>

<dd> <b>See Also</b> <code><a href="#DddmpReadNodeIndexCnf()">DddmpReadNodeIndexCnf()</a>
<a href="#DddmpSetVisitedCnf">DddmpSetVisitedCnf</a>
()
<a href="#DddmpVisitedCnf">DddmpVisitedCnf</a>
()
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeCnf.c</CODE></A>

<dt><pre>
<A NAME="DddmpWriteNodeIndexCnfWithTerminalCheck"></A>
static int <I></I>
<B>DddmpWriteNodeIndexCnfWithTerminalCheck</B>(
  DdNode * <b>f</b>, <i>IN: BDD node</i>
  int * <b>cnfIds</b>, <i>IN: possible source for the index to be written</i>
  int  <b>id</b> <i>IN: possible source for the index to be written</i>
)
</pre>
<dd> The index of the node is written in the "next" field of
    a DdNode struct. LSB is not used (set to 0). It is used as 
    "visited" flag in DD traversals. The index corresponds to 
    the BDD node variable if both the node's children are a 
    constant node, otherwise a new CNF variable is used.
<p>

<dd> <b>Side Effects</b> None
<p>

<dd> <b>See Also</b> <code><a href="#DddmpReadNodeIndexCnf()">DddmpReadNodeIndexCnf()</a>
<a href="#DddmpSetVisitedCnf">DddmpSetVisitedCnf</a>
()
<a href="#DddmpVisitedCnf">DddmpVisitedCnf</a>
()
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpNodeCnf.c</CODE></A>

<dt><pre>
<A NAME="DddmpWriteNodeIndexCnf"></A>
int <I></I>
<B>DddmpWriteNodeIndexCnf</B>(
  DdNode * <b>f</b>, <i>IN: BDD node</i>
  int  <b>id</b> <i>IN: index to be written</i>
)
</pre>
<dd> The index of the node is written in the "next" field of
    a DdNode struct. LSB is not used (set to 0). It is used as 
    "visited" flag in DD traversals.
<p>

<dd> <b>Side Effects</b> None
<p>

<dd> <b>See Also</b> <code><a href="#DddmpReadNodeIndexCnf()">DddmpReadNodeIndexCnf()</a>
<a href="#DddmpSetVisitedCnf">DddmpSetVisitedCnf</a>
()
<a href="#DddmpVisitedCnf">DddmpVisitedCnf</a>
()
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpNodeCnf.c</CODE></A>

<dt><pre>
<A NAME="DddmpWriteNodeIndexCnf"></A>
static int <I></I>
<B>DddmpWriteNodeIndexCnf</B>(
  DdNode * <b>f</b>, <i>IN: BDD node</i>
  int * <b>cnfIds</b>, <i>IN: possible source for the index to be written</i>
  int  <b>id</b> <i>IN: possible source for the index to be written</i>
)
</pre>
<dd> The index of the node is written in the "next" field of
    a DdNode struct. LSB is not used (set to 0). It is used as 
    "visited" flag in DD traversals. The index corresponds to 
    the BDD node variable if both the node's children are a 
    constant node, otherwise a new CNF variable is used.
<p>

<dd> <b>Side Effects</b> None
<p>

<dd> <b>See Also</b> <code><a href="#DddmpReadNodeIndexCnf()">DddmpReadNodeIndexCnf()</a>
<a href="#DddmpSetVisitedCnf">DddmpSetVisitedCnf</a>
()
<a href="#DddmpVisitedCnf">DddmpVisitedCnf</a>
()
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeCnf.c</CODE></A>

<dt><pre>
<A NAME="DddmpWriteNodeIndex"></A>
void <I></I>
<B>DddmpWriteNodeIndex</B>(
  DdNode * <b>f</b>, <i>IN: BDD node</i>
  int  <b>id</b> <i>IN: index to be written</i>
)
</pre>
<dd> The index of the node is written in the "next" field of
    a DdNode struct. LSB is not used (set to 0). It is used as 
    "visited" flag in DD traversals.
<p>

<dd> <b>Side Effects</b> None
<p>

<dd> <b>See Also</b> <code><a href="#DddmpReadNodeIndex()">DddmpReadNodeIndex()</a>
<a href="#DddmpSetVisited">DddmpSetVisited</a>
()
<a href="#DddmpVisited">DddmpVisited</a>
()
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeBdd.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeBdd.c</CODE></A>

<dt><pre>
<A NAME="Dddmp_Bin2Text"></A>
int <I></I>
<B>Dddmp_Bin2Text</B>(
  char * <b>filein</b>, <i>IN: name of binary file</i>
  char * <b>fileout</b> <i>IN: name of ASCII file</i>
)
</pre>
<dd> Converts from binary to ASCII format. A BDD array is loaded and
    and stored to the target file.
<p>

<dd> <b>Side Effects</b> None
<p>

<dd> <b>See Also</b> <code><a href="#Dddmp_Text2Bin()">Dddmp_Text2Bin()</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpConvert.c"TARGET="ABSTRACT"><CODE>dddmpConvert.c</CODE></A>

<dt><pre>
<A NAME="Dddmp_Text2Bin"></A>
int <I></I>
<B>Dddmp_Text2Bin</B>(
  char * <b>filein</b>, <i>IN: name of ASCII file</i>
  char * <b>fileout</b> <i>IN: name of binary file</i>
)
</pre>
<dd> Converts from ASCII to binary format. A BDD array is loaded and
    and stored to the target file.
<p>

<dd> <b>Side Effects</b> None
<p>

<dd> <b>See Also</b> <code><a href="#Dddmp_Bin2Text()">Dddmp_Bin2Text()</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpConvert.c"TARGET="ABSTRACT"><CODE>dddmpConvert.c</CODE></A>

<dt><pre>
<A NAME="Dddmp_cuddAddArrayLoad"></A>
int <I></I>
<B>Dddmp_cuddAddArrayLoad</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  Dddmp_RootMatchType  <b>rootMatchMode</b>, <i>IN: storing mode selector</i>
  char ** <b>rootmatchnames</b>, <i>IN: sorted names for loaded roots</i>
  Dddmp_VarMatchType  <b>varMatchMode</b>, <i>IN: storing mode selector</i>
  char ** <b>varmatchnames</b>, <i>IN: array of variable names, by ids</i>
  int * <b>varmatchauxids</b>, <i>IN: array of variable auxids, by ids</i>
  int * <b>varcomposeids</b>, <i>IN: array of new ids, by ids</i>
  int  <b>mode</b>, <i>IN: requested input file format</i>
  char * <b>file</b>, <i>IN: file name</i>
  FILE * <b>fp</b>, <i>IN: file pointer</i>
  DdNode *** <b>pproots</b> <i>OUT: array of returned BDD roots</i>
)
</pre>
<dd> Reads a dump file representing the argument ADDs. See 
    BDD load functions for detailed explanation.
<p>

<dd> <b>Side Effects</b> A vector of pointers to DD nodes is allocated and freed.
<p>

<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddArrayStore">Dddmp_cuddBddArrayStore</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpLoad.c"TARGET="ABSTRACT"><CODE>dddmpLoad.c</CODE></A>

<dt><pre>
<A NAME="Dddmp_cuddAddArrayStore"></A>
int <I></I>
<B>Dddmp_cuddAddArrayStore</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  char * <b>ddname</b>, <i>IN: DD name (or NULL)</i>
  int  <b>nRoots</b>, <i>IN: number of output BDD roots to be stored</i>
  DdNode ** <b>f</b>, <i>IN: array of ADD roots to be stored</i>
  char ** <b>rootnames</b>, <i>IN: array of root names (or NULL)</i>
  char ** <b>varnames</b>, <i>IN: array of variable names (or NULL)</i>
  int * <b>auxids</b>, <i>IN: array of converted var IDs</i>
  int  <b>mode</b>, <i>IN: storing mode selector</i>
  Dddmp_VarInfoType  <b>varinfo</b>, <i>IN: extra info for variables in text mode</i>
  char * <b>fname</b>, <i>IN: File name</i>
  FILE * <b>fp</b> <i>IN: File pointer to the store file</i>
)
</pre>
<dd> Dumps the argument array of ADDs to file. Dumping is
    either in text or binary form. see the corresponding BDD dump 
    function for further details.
<p>

<dd> <b>Side Effects</b> Nodes are temporarily removed from the unique hash
    table. They are re-linked after the store operation in a 
    modified order.
<p>

<dd> <b>See Also</b> <code><a href="#Dddmp_cuddAddStore">Dddmp_cuddAddStore</a>
<a href="#Dddmp_cuddAddLoad">Dddmp_cuddAddLoad</a>
<a href="#Dddmp_cuddAddArrayLoad">Dddmp_cuddAddArrayLoad</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreAdd.c"TARGET="ABSTRACT"><CODE>dddmpStoreAdd.c</CODE></A>

<dt><pre>
<A NAME="Dddmp_cuddAddLoad"></A>
DdNode * <I></I>
<B>Dddmp_cuddAddLoad</B>(
  DdManager * <b>ddMgr</b>, <i>IN: Manager</i>
  Dddmp_VarMatchType  <b>varMatchMode</b>, <i>IN: storing mode selector</i>
  char ** <b>varmatchnames</b>, <i>IN: array of variable names by IDs</i>
  int * <b>varmatchauxids</b>, <i>IN: array of variable auxids by IDs</i>
  int * <b>varcomposeids</b>, <i>IN: array of new ids by IDs</i>
  int  <b>mode</b>, <i>IN: requested input file format</i>
  char * <b>file</b>, <i>IN: file name</i>
  FILE * <b>fp</b> <i>IN: file pointer</i>
)
</pre>
<dd> Reads a dump file representing the argument ADD.
    Dddmp_cuddAddArrayLoad is used through a dummy array.
<p>

<dd> <b>Side Effects</b> A vector of pointers to DD nodes is allocated and freed.
<p>

<dd> <b>See Also</b> <code><a href="#Dddmp_cuddAddStore">Dddmp_cuddAddStore</a>
<a href="#Dddmp_cuddAddArrayLoad">Dddmp_cuddAddArrayLoad</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpLoad.c"TARGET="ABSTRACT"><CODE>dddmpLoad.c</CODE></A>

<dt><pre>
<A NAME="Dddmp_cuddAddStore"></A>
int <I></I>
<B>Dddmp_cuddAddStore</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  char * <b>ddname</b>, <i>IN: DD name (or NULL)</i>
  DdNode * <b>f</b>, <i>IN: ADD root to be stored</i>
  char ** <b>varnames</b>, <i>IN: array of variable names (or NULL)</i>
  int * <b>auxids</b>, <i>IN: array of converted var ids</i>
  int  <b>mode</b>, <i>IN: storing mode selector</i>
  Dddmp_VarInfoType  <b>varinfo</b>, <i>IN: extra info for variables in text mode</i>
  char * <b>fname</b>, <i>IN: File name</i>
  FILE * <b>fp</b> <i>IN: File pointer to the store file</i>
)
</pre>
<dd> Dumps the argument ADD to file. Dumping is done through
    Dddmp_cuddAddArrayStore, And a dummy array of 1 ADD root is
    used for this purpose.
<p>

<dd> <b>Side Effects</b> Nodes are temporarily removed from unique hash. They are 
    re-linked after the store operation in a modified order.
<p>

<dd> <b>See Also</b> <code><a href="#Dddmp_cuddAddLoad">Dddmp_cuddAddLoad</a>
<a href="#Dddmp_cuddAddArrayLoad">Dddmp_cuddAddArrayLoad</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreAdd.c"TARGET="ABSTRACT"><CODE>dddmpStoreAdd.c</CODE></A>

<dt><pre>
<A NAME="Dddmp_cuddBddArrayLoadCnf"></A>
int <I></I>
<B>Dddmp_cuddBddArrayLoadCnf</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  Dddmp_RootMatchType  <b>rootmatchmode</b>, <i>IN: storing mode selector</i>
  char ** <b>rootmatchnames</b>, <i>IN: sorted names for loaded roots</i>
  Dddmp_VarMatchType  <b>varmatchmode</b>, <i>IN: storing mode selector</i>
  char ** <b>varmatchnames</b>, <i>IN: array of variable names, by IDs</i>
  int * <b>varmatchauxids</b>, <i>IN: array of variable auxids, by IDs</i>
  int * <b>varcomposeids</b>, <i>IN: array of new ids, by IDs</i>
  int  <b>mode</b>, <i>IN: computation Mode</i>
  char * <b>file</b>, <i>IN: file name</i>
  FILE * <b>fp</b>, <i>IN: file pointer</i>
  DdNode *** <b>rootsPtrPtr</b>, <i>OUT: array of returned BDD roots</i>
  int * <b>nRoots</b> <i>OUT: number of BDDs returned</i>
)
</pre>
<dd> Reads a dump file representing the argument BDD in a
    CNF formula.
<p>

<dd> <b>Side Effects</b> A vector of pointers to DD nodes is allocated and freed.
<p>

<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddArrayLoad">Dddmp_cuddBddArrayLoad</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpLoadCnf.c"TARGET="ABSTRACT"><CODE>dddmpLoadCnf.c</CODE></A>

<dt><pre>
<A NAME="Dddmp_cuddBddArrayLoad"></A>
int <I></I>
<B>Dddmp_cuddBddArrayLoad</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  Dddmp_RootMatchType  <b>rootMatchMode</b>, <i>IN: storing mode selector</i>
  char ** <b>rootmatchnames</b>, <i>IN: sorted names for loaded roots</i>
  Dddmp_VarMatchType  <b>varMatchMode</b>, <i>IN: storing mode selector</i>
  char ** <b>varmatchnames</b>, <i>IN: array of variable names, by ids</i>
  int * <b>varmatchauxids</b>, <i>IN: array of variable auxids, by ids</i>
  int * <b>varcomposeids</b>, <i>IN: array of new ids, by ids</i>
  int  <b>mode</b>, <i>IN: requested input file format</i>
  char * <b>file</b>, <i>IN: file name</i>
  FILE * <b>fp</b>, <i>IN: file pointer</i>
  DdNode *** <b>pproots</b> <i>OUT: array of returned BDD roots</i>
)
</pre>
<dd> Reads a dump file representing the argument BDDs. The header is
    common to both text and binary mode. The node list is either 
    in text or binary format. A dynamic vector of DD pointers 
    is allocated to support conversion from DD indexes to pointers.
    Several criteria are supported for variable match between file
    and dd manager. Several changes/permutations/compositions are allowed
    for variables while loading DDs. Variable of the dd manager are allowed 
    to match with variables on file on ids, permids, varnames, 
    varauxids; also direct composition between ids and 
    composeids is supported. More in detail:
    <ol>
    <li> varMatchMode=DDDMP_VAR_MATCHIDS <p>
    allows the loading of a DD keeping variable IDs unchanged
    (regardless of the variable ordering of the reading manager); this
    is useful, for example, when swapping DDs to file and restoring them
    later from file, after possible variable reordering activations.
    
    <li> varMatchMode=DDDMP_VAR_MATCHPERMIDS <p>
    is used to allow variable match according to the position in the
    ordering.
    
    <li> varMatchMode=DDDMP_VAR_MATCHNAMES <p>
    requires a non NULL varmatchnames parameter; this is a vector of
    strings in one-to-one correspondence with variable IDs of the
    reading manager. Variables in the DD file read are matched with
    manager variables according to their name (a non NULL varnames
    parameter was required while storing the DD file).
    
    <li> varMatchMode=DDDMP_VAR_MATCHIDS <p>
    has a meaning similar to DDDMP_VAR_MATCHNAMES, but integer auxiliary
    IDs are used instead of strings; the additional non NULL
    varmatchauxids parameter is needed.
    
    <li> varMatchMode=DDDMP_VAR_COMPOSEIDS <p>
    uses the additional varcomposeids parameter is used as array of
    variable ids to be composed with ids stored in file.
    </ol>
    
    In the present implementation, the array varnames (3), varauxids (4)
    and composeids (5) need to have one entry for each variable in the 
    DD manager (NULL pointers are allowed for unused variables
    in varnames). Hence variables need to be already present in the 
    manager. All arrays are sorted according to IDs.

    All the loaded BDDs are referenced before returning them.
<p>

<dd> <b>Side Effects</b> A vector of pointers to DD nodes is allocated and freed.
<p>

<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddArrayStore">Dddmp_cuddBddArrayStore</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpLoad.c"TARGET="ABSTRACT"><CODE>dddmpLoad.c</CODE></A>

<dt><pre>
<A NAME="Dddmp_cuddBddArrayStoreBlif"></A>
int <I></I>
<B>Dddmp_cuddBddArrayStoreBlif</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  int  <b>nroots</b>, <i>IN: number of output BDD roots to be stored</i>
  DdNode ** <b>f</b>, <i>IN: array of BDD roots to be stored</i>
  char ** <b>inputNames</b>, <i>IN: array of variable names (or NULL)</i>
  char ** <b>outputNames</b>, <i>IN: array of root names (or NULL)</i>
  char * <b>modelName</b>, <i>IN: Model Name</i>
  char * <b>fname</b>, <i>IN: File name</i>
  FILE * <b>fp</b> <i>IN: File pointer to the store file</i>
)
</pre>
<dd> Dumps the argument BDD to file.
    Dumping is done through Dddmp_cuddBddArrayStoreBLif.
    A dummy array of 1 BDD root is used for this purpose.
<p>

<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddArrayStorePrefix">Dddmp_cuddBddArrayStorePrefix</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreMisc.c"TARGET="ABSTRACT"><CODE>dddmpStoreMisc.c</CODE></A>

<dt><pre>
<A NAME="Dddmp_cuddBddArrayStoreCnf"></A>
int <I></I>
<B>Dddmp_cuddBddArrayStoreCnf</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  DdNode ** <b>f</b>, <i>IN: array of BDD roots to be stored</i>
  int  <b>rootN</b>, <i>IN: # output BDD roots to be stored</i>
  Dddmp_DecompCnfStoreType  <b>mode</b>, <i>IN: format selection</i>
  int  <b>noHeader</b>, <i>IN: do not store header iff 1</i>
  char ** <b>varNames</b>, <i>IN: array of variable names (or NULL)</i>
  int * <b>bddIds</b>, <i>IN: array of converted var IDs</i>
  int * <b>bddAuxIds</b>, <i>IN: array of BDD node Auxiliary Ids</i>
  int * <b>cnfIds</b>, <i>IN: array of converted var IDs</i>
  int  <b>idInitial</b>, <i>IN: starting id for cutting variables</i>
  int  <b>edgeInTh</b>, <i>IN: Max # Incoming Edges</i>
  int  <b>pathLengthTh</b>, <i>IN: Max Path Length</i>
  char * <b>fname</b>, <i>IN: file name</i>
  FILE * <b>fp</b>, <i>IN: pointer to the store file</i>
  int * <b>clauseNPtr</b>, <i>OUT: number of clause stored</i>
  int * <b>varNewNPtr</b> <i>OUT: number of new variable created</i>
)
</pre>
<dd> Dumps the argument array of BDDs to file.
<p>

<dd> <b>Side Effects</b> Nodes are temporarily removed from the unique hash
    table. They are re-linked after the store operation in a 
    modified order.
    Three methods are allowed:
    * NodeByNode method: Insert a cut-point for each BDD node (but the
                         terminal nodes)
    * MaxtermByMaxterm method: Insert no cut-points, i.e. the off-set of
                               trhe function is stored
    * Best method: Tradeoff between the previous two methods.
      Auxiliary variables, i.e., cut points are inserted following these
      criterias:
      * edgeInTh
        indicates the maximum number of incoming edges up to which
        no cut point (auxiliary variable) is inserted.
        If edgeInTh:
        * is equal to -1 no cut point due to incoming edges are inserted
          (MaxtermByMaxterm method.)
	* is equal to 0 a cut point is inserted for each node with a single
          incoming edge, i.e., each node, (NodeByNode method).
	* is equal to n a cut point is inserted for each node with (n+1)
          incoming edges.
      * pathLengthTh
        indicates the maximum length path up to which no cut points
        (auxiliary variable) is inserted.
        If the path length between two nodes exceeds this value, a cut point
        is inserted.
        If pathLengthTh:
        * is equal to -1 no cut point due path length are inserted
          (MaxtermByMaxterm method.)
	* is equal to 0 a cut point is inserted for each node (NodeByNode
          method).
	* is equal to n a cut point is inserted on path whose length is
          equal to (n+1).
        Notice that the maximum number of literals in a clause is equal
        to (pathLengthTh + 2), i.e., for each path we have to keep into
        account a CNF variable for each node plus 2 added variables for
        the bottom and top-path cut points.
    The stored file can contain a file header or not depending on the
    noHeader parameter (IFF 0, usual setting, the header is usually stored.
    This option can be useful in storing multiple BDDs, as separate BDDs,
    on the same file leaving the opening of the file to the caller.
<p>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreCnf.c"TARGET="ABSTRACT"><CODE>dddmpStoreCnf.c</CODE></A>

<dt><pre>
<A NAME="Dddmp_cuddBddArrayStorePrefix"></A>
int <I></I>
<B>Dddmp_cuddBddArrayStorePrefix</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  int  <b>nroots</b>, <i>IN: number of output BDD roots to be stored</i>
  DdNode ** <b>f</b>, <i>IN: array of BDD roots to be stored</i>
  char ** <b>inputNames</b>, <i>IN: array of variable names (or NULL)</i>
  char ** <b>outputNames</b>, <i>IN: array of root names (or NULL)</i>
  char * <b>modelName</b>, <i>IN: Model Name</i>
  char * <b>fname</b>, <i>IN: File name</i>
  FILE * <b>fp</b> <i>IN: File pointer to the store file</i>
)
</pre>
<dd> Dumps the argument BDD to file.
    Dumping is done through Dddmp_cuddBddArrayStorePrefix.
    A dummy array of 1 BDD root is used for this purpose.
<p>

<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddArrayStore">Dddmp_cuddBddArrayStore</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreMisc.c"TARGET="ABSTRACT"><CODE>dddmpStoreMisc.c</CODE></A>

<dt><pre>
<A NAME="Dddmp_cuddBddArrayStoreSmv"></A>
int <I></I>
<B>Dddmp_cuddBddArrayStoreSmv</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  int  <b>nroots</b>, <i>IN: number of output BDD roots to be stored</i>
  DdNode ** <b>f</b>, <i>IN: array of BDD roots to be stored</i>
  char ** <b>inputNames</b>, <i>IN: array of variable names (or NULL)</i>
  char ** <b>outputNames</b>, <i>IN: array of root names (or NULL)</i>
  char * <b>modelName</b>, <i>IN: Model Name</i>
  char * <b>fname</b>, <i>IN: File name</i>
  FILE * <b>fp</b> <i>IN: File pointer to the store file</i>
)
</pre>
<dd> Dumps the argument BDD to file.
    Dumping is done through Dddmp_cuddBddArrayStorePrefix.
    A dummy array of 1 BDD root is used for this purpose.
<p>

<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddArrayStore">Dddmp_cuddBddArrayStore</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreMisc.c"TARGET="ABSTRACT"><CODE>dddmpStoreMisc.c</CODE></A>

<dt><pre>
<A NAME="Dddmp_cuddBddArrayStore"></A>
int <I></I>
<B>Dddmp_cuddBddArrayStore</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  char * <b>ddname</b>, <i>IN: dd name (or NULL)</i>
  int  <b>nRoots</b>, <i>IN: number of output BDD roots to be stored</i>
  DdNode ** <b>f</b>, <i>IN: array of BDD roots to be stored</i>
  char ** <b>rootnames</b>, <i>IN: array of root names (or NULL)</i>
  char ** <b>varnames</b>, <i>IN: array of variable names (or NULL)</i>
  int * <b>auxids</b>, <i>IN: array of converted var IDs</i>
  int  <b>mode</b>, <i>IN: storing mode selector</i>
  Dddmp_VarInfoType  <b>varinfo</b>, <i>IN: extra info for variables in text mode</i>
  char * <b>fname</b>, <i>IN: File name</i>
  FILE * <b>fp</b> <i>IN: File pointer to the store file</i>
)
</pre>
<dd> Dumps the argument array of BDDs to file. Dumping is either 
    in text or binary form.  BDDs are stored to the fp (already 
    open) file if not NULL. Otherwise the file whose name is 
    fname is opened in write mode. The header has the same format 
    for both textual and binary dump. Names are allowed for input 
    variables (vnames) and for represented functions (rnames). 
    For sake of generality and because of dynamic variable 
    ordering both variable IDs and permuted IDs are included. 
    New IDs are also supported (auxids). Variables are identified 
    with incremental numbers. according with their positiom in 
    the support set. In text mode, an extra info may be added, 
    chosen among the following options: name, ID, PermID, or an 
    auxiliary id. Since conversion from DD pointers to integers 
    is required, DD nodes are temporarily removed from the unique
    hash table. This allows the use of the next field to store 
    node IDs.
<p>

<dd> <b>Side Effects</b> Nodes are temporarily removed from the unique hash
    table. They are re-linked after the store operation in a 
    modified order.
<p>

<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddStore">Dddmp_cuddBddStore</a>
<a href="#Dddmp_cuddBddLoad">Dddmp_cuddBddLoad</a>
<a href="#Dddmp_cuddBddArrayLoad">Dddmp_cuddBddArrayLoad</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreBdd.c"TARGET="ABSTRACT"><CODE>dddmpStoreBdd.c</CODE></A>

<dt><pre>
<A NAME="Dddmp_cuddBddDisplayBinary"></A>
int <I></I>
<B>Dddmp_cuddBddDisplayBinary</B>(
  char * <b>fileIn</b>, <i>IN: name of binary file</i>
  char * <b>fileOut</b> <i>IN: name of text file</i>
)
</pre>
<dd> Display a binary dump file in a text file
<p>

<dd> <b>Side Effects</b> None
<p>

<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddStore">Dddmp_cuddBddStore</a>
<a href="#Dddmp_cuddBddLoad">Dddmp_cuddBddLoad</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDbg.c"TARGET="ABSTRACT"><CODE>dddmpDbg.c</CODE></A>

<dt><pre>
<A NAME="Dddmp_cuddBddLoadCnf"></A>
int <I></I>
<B>Dddmp_cuddBddLoadCnf</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  Dddmp_VarMatchType  <b>varmatchmode</b>, <i>IN: storing mode selector</i>
  char ** <b>varmatchnames</b>, <i>IN: array of variable names, by IDs</i>
  int * <b>varmatchauxids</b>, <i>IN: array of variable auxids, by IDs</i>
  int * <b>varcomposeids</b>, <i>IN: array of new ids accessed, by IDs</i>
  int  <b>mode</b>, <i>IN: computation mode</i>
  char * <b>file</b>, <i>IN: file name</i>
  FILE * <b>fp</b>, <i>IN: file pointer</i>
  DdNode *** <b>rootsPtrPtr</b>, <i>OUT: array of returned BDD roots</i>
  int * <b>nRoots</b> <i>OUT: number of BDDs returned</i>
)
</pre>
<dd> Reads a dump file representing the argument BDD in a
    CNF formula.
    Dddmp_cuddBddArrayLoadCnf is used through a dummy array.
    The results is returned in different formats depending on the 
    mode selection:
      IFF mode == 0 Return the Clauses without Conjunction
      IFF mode == 1 Return the sets of BDDs without Quantification
      IFF mode == 2 Return the sets of BDDs AFTER Existential Quantification
<p>

<dd> <b>Side Effects</b> A vector of pointers to DD nodes is allocated and freed.
<p>

<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddLoad">Dddmp_cuddBddLoad</a>
<a href="#Dddmp_cuddBddArrayLoad">Dddmp_cuddBddArrayLoad</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpLoadCnf.c"TARGET="ABSTRACT"><CODE>dddmpLoadCnf.c</CODE></A>

<dt><pre>
<A NAME="Dddmp_cuddBddLoad"></A>
DdNode * <I></I>
<B>Dddmp_cuddBddLoad</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  Dddmp_VarMatchType  <b>varMatchMode</b>, <i>IN: storing mode selector</i>
  char ** <b>varmatchnames</b>, <i>IN: array of variable names - by IDs</i>
  int * <b>varmatchauxids</b>, <i>IN: array of variable auxids - by IDs</i>
  int * <b>varcomposeids</b>, <i>IN: array of new ids accessed - by IDs</i>
  int  <b>mode</b>, <i>IN: requested input file format</i>
  char * <b>file</b>, <i>IN: file name</i>
  FILE * <b>fp</b> <i>IN: file pointer</i>
)
</pre>
<dd> Reads a dump file representing the argument BDD.
    Dddmp_cuddBddArrayLoad is used through a dummy array (see this
    function's description for more details).
    Mode, the requested input file format, is checked against 
    the file format.
    The loaded BDDs is referenced before returning it.
<p>

<dd> <b>Side Effects</b> A vector of pointers to DD nodes is allocated and freed.
<p>

<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddStore">Dddmp_cuddBddStore</a>
<a href="#Dddmp_cuddBddArrayLoad">Dddmp_cuddBddArrayLoad</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpLoad.c"TARGET="ABSTRACT"><CODE>dddmpLoad.c</CODE></A>

<dt><pre>
<A NAME="Dddmp_cuddBddStoreBlif"></A>
int <I></I>
<B>Dddmp_cuddBddStoreBlif</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  int  <b>nRoots</b>, <i>IN: Number of BDD roots</i>
  DdNode * <b>f</b>, <i>IN: BDD root to be stored</i>
  char ** <b>inputNames</b>, <i>IN: Array of variable names</i>
  char ** <b>outputNames</b>, <i>IN: Array of root names</i>
  char * <b>modelName</b>, <i>IN: Model Name</i>
  char * <b>fileName</b>, <i>IN: File name</i>
  FILE * <b>fp</b> <i>IN: File pointer to the store file</i>
)
</pre>
<dd> Dumps the argument BDD to file.
    Dumping is done through Dddmp_cuddBddArrayStoreBlif.
    A dummy array of 1 BDD root is used for this purpose.
<p>

<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddStorePrefix">Dddmp_cuddBddStorePrefix</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreMisc.c"TARGET="ABSTRACT"><CODE>dddmpStoreMisc.c</CODE></A>

<dt><pre>
<A NAME="Dddmp_cuddBddStoreCnf"></A>
int <I></I>
<B>Dddmp_cuddBddStoreCnf</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  DdNode * <b>f</b>, <i>IN: BDD root to be stored</i>
  Dddmp_DecompCnfStoreType  <b>mode</b>, <i>IN: format selection</i>
  int  <b>noHeader</b>, <i>IN: do not store header iff 1</i>
  char ** <b>varNames</b>, <i>IN: array of variable names (or NULL)</i>
  int * <b>bddIds</b>, <i>IN: array of var ids</i>
  int * <b>bddAuxIds</b>, <i>IN: array of BDD node Auxiliary Ids</i>
  int * <b>cnfIds</b>, <i>IN: array of CNF var ids</i>
  int  <b>idInitial</b>, <i>IN: starting id for cutting variables</i>
  int  <b>edgeInTh</b>, <i>IN: Max # Incoming Edges</i>
  int  <b>pathLengthTh</b>, <i>IN: Max Path Length</i>
  char * <b>fname</b>, <i>IN: file name</i>
  FILE * <b>fp</b>, <i>IN: pointer to the store file</i>
  int * <b>clauseNPtr</b>, <i>OUT: number of clause stored</i>
  int * <b>varNewNPtr</b> <i>OUT: number of new variable created</i>
)
</pre>
<dd> Dumps the argument BDD to file.
    This task is performed by calling the function
    Dddmp_cuddBddArrayStoreCnf.
<p>

<dd> <b>Side Effects</b> Nodes are temporarily removed from unique hash. They are
    re-linked after the store operation in a modified order.
<p>

<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddArrayStoreCnf">Dddmp_cuddBddArrayStoreCnf</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreCnf.c"TARGET="ABSTRACT"><CODE>dddmpStoreCnf.c</CODE></A>

<dt><pre>
<A NAME="Dddmp_cuddBddStorePrefix"></A>
int <I></I>
<B>Dddmp_cuddBddStorePrefix</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  int  <b>nRoots</b>, <i>IN: Number of BDD roots</i>
  DdNode * <b>f</b>, <i>IN: BDD root to be stored</i>
  char ** <b>inputNames</b>, <i>IN: Array of variable names</i>
  char ** <b>outputNames</b>, <i>IN: Array of root names</i>
  char * <b>modelName</b>, <i>IN: Model Name</i>
  char * <b>fileName</b>, <i>IN: File name</i>
  FILE * <b>fp</b> <i>IN: File pointer to the store file</i>
)
</pre>
<dd> Dumps the argument BDD to file.
    Dumping is done through Dddmp_cuddBddArrayStorePrefix.
    A dummy array of 1 BDD root is used for this purpose.
<p>

<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddStore">Dddmp_cuddBddStore</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreMisc.c"TARGET="ABSTRACT"><CODE>dddmpStoreMisc.c</CODE></A>

<dt><pre>
<A NAME="Dddmp_cuddBddStoreSmv"></A>
int <I></I>
<B>Dddmp_cuddBddStoreSmv</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  int  <b>nRoots</b>, <i>IN: Number of BDD roots</i>
  DdNode * <b>f</b>, <i>IN: BDD root to be stored</i>
  char ** <b>inputNames</b>, <i>IN: Array of variable names</i>
  char ** <b>outputNames</b>, <i>IN: Array of root names</i>
  char * <b>modelName</b>, <i>IN: Model Name</i>
  char * <b>fileName</b>, <i>IN: File name</i>
  FILE * <b>fp</b> <i>IN: File pointer to the store file</i>
)
</pre>
<dd> Dumps the argument BDD to file.
    Dumping is done through Dddmp_cuddBddArrayStorePrefix.
    A dummy array of 1 BDD root is used for this purpose.
<p>

<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddStore">Dddmp_cuddBddStore</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreMisc.c"TARGET="ABSTRACT"><CODE>dddmpStoreMisc.c</CODE></A>

<dt><pre>
<A NAME="Dddmp_cuddBddStore"></A>
int <I></I>
<B>Dddmp_cuddBddStore</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  char * <b>ddname</b>, <i>IN: DD name (or NULL)</i>
  DdNode * <b>f</b>, <i>IN: BDD root to be stored</i>
  char ** <b>varnames</b>, <i>IN: array of variable names (or NULL)</i>
  int * <b>auxids</b>, <i>IN: array of converted var ids</i>
  int  <b>mode</b>, <i>IN: storing mode selector</i>
  Dddmp_VarInfoType  <b>varinfo</b>, <i>IN: extra info for variables in text mode</i>
  char * <b>fname</b>, <i>IN: File name</i>
  FILE * <b>fp</b> <i>IN: File pointer to the store file</i>
)
</pre>
<dd> Dumps the argument BDD to file. Dumping is done through
    Dddmp_cuddBddArrayStore. A dummy array of 1 BDD root is
    used for this purpose.
<p>

<dd> <b>Side Effects</b> Nodes are temporarily removed from unique hash. They are
    re-linked after the store operation in a modified order.
<p>

<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddLoad">Dddmp_cuddBddLoad</a>
<a href="#Dddmp_cuddBddArrayLoad">Dddmp_cuddBddArrayLoad</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreBdd.c"TARGET="ABSTRACT"><CODE>dddmpStoreBdd.c</CODE></A>

<dt><pre>
<A NAME="Dddmp_cuddHeaderLoadCnf"></A>
int <I></I>
<B>Dddmp_cuddHeaderLoadCnf</B>(
  int * <b>nVars</b>, <i>OUT: number of DD variables</i>
  int * <b>nsuppvars</b>, <i>OUT: number of support variables</i>
  char *** <b>suppVarNames</b>, <i>OUT: array of support variable names</i>
  char *** <b>orderedVarNames</b>, <i>OUT: array of variable names</i>
  int ** <b>varIds</b>, <i>OUT: array of variable ids</i>
  int ** <b>varComposeIds</b>, <i>OUT: array of permids ids</i>
  int ** <b>varAuxIds</b>, <i>OUT: array of variable aux ids</i>
  int * <b>nRoots</b>, <i>OUT: number of root in the file</i>
  char * <b>file</b>, <i>IN: file name</i>
  FILE * <b>fp</b> <i>IN: file pointer</i>
)
</pre>
<dd> Reads the header of a dump file representing the argument BDDs. 
    Returns main information regarding DD type stored in the file,
    the variable ordering used, the number of variables, etc.
    It reads only the header of the file NOT the BDD/ADD section.
<p>

<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddArrayLoad">Dddmp_cuddBddArrayLoad</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpLoadCnf.c"TARGET="ABSTRACT"><CODE>dddmpLoadCnf.c</CODE></A>

<dt><pre>
<A NAME="Dddmp_cuddHeaderLoad"></A>
int <I></I>
<B>Dddmp_cuddHeaderLoad</B>(
  Dddmp_DecompType * <b>ddType</b>, <i>OUT: selects the proper decomp type</i>
  int * <b>nVars</b>, <i>OUT: number of DD variables</i>
  int * <b>nsuppvars</b>, <i>OUT: number of support variables</i>
  char *** <b>suppVarNames</b>, <i>OUT: array of support variable names</i>
  char *** <b>orderedVarNames</b>, <i>OUT: array of variable names</i>
  int ** <b>varIds</b>, <i>OUT: array of variable ids</i>
  int ** <b>varComposeIds</b>, <i>OUT: array of permids ids</i>
  int ** <b>varAuxIds</b>, <i>OUT: array of variable aux ids</i>
  int * <b>nRoots</b>, <i>OUT: number of root in the file</i>
  char * <b>file</b>, <i>IN: file name</i>
  FILE * <b>fp</b> <i>IN: file pointer</i>
)
</pre>
<dd> Reads the header of a dump file representing the argument BDDs.
    Returns main information regarding DD type stored in the file,
    the variable ordering used, the number of variables, etc.
    It reads only the header of the file NOT the BDD/ADD section.
<p>

<dd> <b>See Also</b> <code><a href="#Dddmp_cuddBddArrayLoad">Dddmp_cuddBddArrayLoad</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpLoad.c"TARGET="ABSTRACT"><CODE>dddmpLoad.c</CODE></A>

<dt><pre>
<A NAME="FindVarname"></A>
int <I></I>
<B>FindVarname</B>(
  char * <b>name</b>, <i>IN: name to look for</i>
  char ** <b>array</b>, <i>IN: search array</i>
  int  <b>n</b> <i>IN: size of the array</i>
)
</pre>
<dd> Binary search of a name within a sorted array of strings.
    Used when matching names of variables.
<p>

<dd> <b>Side Effects</b> None
<p>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpUtil.c"TARGET="ABSTRACT"><CODE>dddmpUtil.c</CODE></A>

<dt><pre>
<A NAME="NodeBinaryStoreBdd"></A>
static int <I></I>
<B>NodeBinaryStoreBdd</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  DdNode * <b>f</b>, <i>IN: DD node to be stored</i>
  int  <b>mode</b>, <i>IN: store mode</i>
  int * <b>supportids</b>, <i>IN: internal ids for variables</i>
  char ** <b>varnames</b>, <i>IN: names of variables: to be stored with nodes</i>
  int * <b>outids</b>, <i>IN: output ids for variables</i>
  FILE * <b>fp</b>, <i>IN: store file</i>
  int  <b>idf</b>, <i>IN: index of the node</i>
  int  <b>vf</b>, <i>IN: variable of the node</i>
  int  <b>idT</b>, <i>IN: index of the Then node</i>
  int  <b>idE</b>, <i>IN: index of the Else node</i>
  int  <b>vT</b>, <i>IN: variable of the Then node</i>
  int  <b>vE</b>, <i>IN: variable of the Else node</i>
  DdNode * <b>T</b>, <i>IN: Then node</i>
  DdNode * <b>E</b> <i>IN: Else node</i>
)
</pre>
<dd> Store 1 0 0 for the terminal node.
    Store id, left child pointer, right pointer for all the other nodes.
    Store every information as coded binary values.
<p>

<dd> <b>Side Effects</b> None
<p>

<dd> <b>See Also</b> <code><a href="#NodeTextStoreBdd">NodeTextStoreBdd</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreBdd.c"TARGET="ABSTRACT"><CODE>dddmpStoreBdd.c</CODE></A>

<dt><pre>
<A NAME="NodeStoreRecurAdd"></A>
static int <I></I>
<B>NodeStoreRecurAdd</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  DdNode * <b>f</b>, <i>IN: DD node to be stored</i>
  int  <b>mode</b>, <i>IN: store mode</i>
  int * <b>supportids</b>, <i>IN: internal ids for variables</i>
  char ** <b>varnames</b>, <i>IN: names of variables: to be stored with nodes</i>
  int * <b>outids</b>, <i>IN: output ids for variables</i>
  FILE * <b>fp</b> <i>IN: store file</i>
)
</pre>
<dd> Stores a node to file in either test or binary mode.<l>
    In text mode a node is represented (on a text line basis) as
    <UL>
    <LI> node-index [var-extrainfo] var-index Then-index Else-index
    </UL>
    
    where all indexes are integer numbers and var-extrainfo 
    (optional redundant field) is either an integer or a string 
    (variable name). Node-index is redundant (due to the node 
    ordering) but we keep it for readability.<p>
    
    In binary mode nodes are represented as a sequence of bytes,
    representing var-index, Then-index, and Else-index in an 
    optimized way. Only the first byte (code) is mandatory. 
    Integer indexes are represented in absolute or relative mode, 
    where relative means offset wrt. a Then/Else node info. 
    Suppose Var(NodeId), Then(NodeId) and Else(NodeId) represent 
    infos about a given node.<p>
    
    The generic "NodeId" node is stored as 

    <UL>
    <LI> code-byte
    <LI> [var-info]
    <LI> [Then-info]
    <LI> [Else-info]
    </UL>

    where code-byte contains bit fields

    <UL>
    <LI>Unused  : 1 bit
    <LI>Variable: 2 bits, one of the following codes
    <UL>
    <LI>DDDMP_ABSOLUTE_ID   var-info = Var(NodeId) follows
    <LI>DDDMP_RELATIVE_ID   Var(NodeId) is represented in relative form as
        var-info = Min(Var(Then(NodeId)),Var(Else(NodeId))) -Var(NodeId)
    <LI>DDDMP_RELATIVE_1    No var-info follows, because
        Var(NodeId) = Min(Var(Then(NodeId)),Var(Else(NodeId)))-1
    <LI>DDDMP_TERMINAL      Node is a terminal, no var info required
    </UL>
    <LI>T       : 2 bits, with codes similar to V
    <UL>
    <LI>DDDMP_ABSOLUTE_ID   Then-info = Then(NodeId) follows
    <LI>DDDMP_RELATIVE_ID   Then(NodeId) is represented in relative form as
          Then-info = Nodeid-Then(NodeId)
    <LI>DDDMP_RELATIVE_1    No info on Then(NodeId) follows, because
          Then(NodeId) = NodeId-1
    <LI>DDDMP_TERMINAL Then Node is a terminal, no info required (for BDDs)
    </UL>
    <LI>Ecompl  : 1 bit, if 1 means complemented edge
    <LI>E       : 2 bits, with codes and meanings as for the Then edge
    </UL>
    var-info, Then-info, Else-info (if required) are represented as unsigned 
    integer values on a sufficient set of bytes (MSByte first).
<p>

<dd> <b>Side Effects</b> None
<p>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreAdd.c"TARGET="ABSTRACT"><CODE>dddmpStoreAdd.c</CODE></A>

<dt><pre>
<A NAME="NodeStoreRecurBdd"></A>
static int <I></I>
<B>NodeStoreRecurBdd</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  DdNode * <b>f</b>, <i>IN: DD node to be stored</i>
  int  <b>mode</b>, <i>IN: store mode</i>
  int * <b>supportids</b>, <i>IN: internal ids for variables</i>
  char ** <b>varnames</b>, <i>IN: names of variables: to be stored with nodes</i>
  int * <b>outids</b>, <i>IN: output ids for variables</i>
  FILE * <b>fp</b> <i>IN: store file</i>
)
</pre>
<dd> Stores a node to file in either test or binary mode.<l>
    In text mode a node is represented (on a text line basis) as
    <UL>
    <LI> node-index [var-extrainfo] var-index Then-index Else-index
    </UL>
    
    where all indexes are integer numbers and var-extrainfo 
    (optional redundant field) is either an integer or a string 
    (variable name). Node-index is redundant (due to the node 
    ordering) but we keep it for readability.<p>
    
    In binary mode nodes are represented as a sequence of bytes,
    representing var-index, Then-index, and Else-index in an 
    optimized way. Only the first byte (code) is mandatory. 
    Integer indexes are represented in absolute or relative mode, 
    where relative means offset wrt. a Then/Else node info. 
    Suppose Var(NodeId), Then(NodeId) and Else(NodeId) represent 
    infos about a given node.<p>
    
    The generic "NodeId" node is stored as 

    <UL>
    <LI> code-byte
    <LI> [var-info]
    <LI> [Then-info]
    <LI> [Else-info]
    </UL>

    where code-byte contains bit fields

    <UL>
    <LI>Unused  : 1 bit
    <LI>Variable: 2 bits, one of the following codes
    <UL>
    <LI>DDDMP_ABSOLUTE_ID   var-info = Var(NodeId) follows
    <LI>DDDMP_RELATIVE_ID   Var(NodeId) is represented in relative form as
        var-info = Min(Var(Then(NodeId)),Var(Else(NodeId))) -Var(NodeId)
    <LI>DDDMP_RELATIVE_1    No var-info follows, because
        Var(NodeId) = Min(Var(Then(NodeId)),Var(Else(NodeId)))-1
    <LI>DDDMP_TERMINAL      Node is a terminal, no var info required
    </UL>
    <LI>T       : 2 bits, with codes similar to V
    <UL>
    <LI>DDDMP_ABSOLUTE_ID   Then-info = Then(NodeId) follows
    <LI>DDDMP_RELATIVE_ID   Then(NodeId) is represented in relative form as
          Then-info = Nodeid-Then(NodeId)
    <LI>DDDMP_RELATIVE_1    No info on Then(NodeId) follows, because
          Then(NodeId) = NodeId-1
    <LI>DDDMP_TERMINAL Then Node is a terminal, no info required (for BDDs)
    </UL>
    <LI>Ecompl  : 1 bit, if 1 means complemented edge
    <LI>E       : 2 bits, with codes and meanings as for the Then edge
    </UL>
    var-info, Then-info, Else-info (if required) are represented as unsigned 
    integer values on a sufficient set of bytes (MSByte first).
<p>

<dd> <b>Side Effects</b> None
<p>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreBdd.c"TARGET="ABSTRACT"><CODE>dddmpStoreBdd.c</CODE></A>

<dt><pre>
<A NAME="NodeTextStoreAdd"></A>
static int <I></I>
<B>NodeTextStoreAdd</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  DdNode * <b>f</b>, <i>IN: DD node to be stored</i>
  int  <b>mode</b>, <i>IN: store mode</i>
  int * <b>supportids</b>, <i>IN: internal ids for variables</i>
  char ** <b>varnames</b>, <i>IN: names of variables: to be stored with nodes</i>
  int * <b>outids</b>, <i>IN: output ids for variables</i>
  FILE * <b>fp</b>, <i>IN: Store file</i>
  int  <b>idf</b>, <i>IN: index of the current node</i>
  int  <b>vf</b>, <i>IN: variable of the current node</i>
  int  <b>idT</b>, <i>IN: index of the Then node</i>
  int  <b>idE</b> <i>IN: index of the Else node</i>
)
</pre>
<dd> Store 1 0 0 for the terminal node.
    Store id, left child pointer, right pointer for all the other nodes.
<p>

<dd> <b>Side Effects</b> None
<p>

<dd> <b>See Also</b> <code><a href="#NodeBinaryStore">NodeBinaryStore</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreAdd.c"TARGET="ABSTRACT"><CODE>dddmpStoreAdd.c</CODE></A>

<dt><pre>
<A NAME="NodeTextStoreBdd"></A>
static int <I></I>
<B>NodeTextStoreBdd</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  DdNode * <b>f</b>, <i>IN: DD node to be stored</i>
  int  <b>mode</b>, <i>IN: store mode</i>
  int * <b>supportids</b>, <i>IN: internal ids for variables</i>
  char ** <b>varnames</b>, <i>IN: names of variables: to be stored with nodes</i>
  int * <b>outids</b>, <i>IN: output ids for variables</i>
  FILE * <b>fp</b>, <i>IN: Store file</i>
  int  <b>idf</b>, <i>IN: index of the current node</i>
  int  <b>vf</b>, <i>IN: variable of the current node</i>
  int  <b>idT</b>, <i>IN: index of the Then node</i>
  int  <b>idE</b> <i>IN: index of the Else node</i>
)
</pre>
<dd> Store 1 0 0 for the terminal node.
    Store id, left child pointer, right pointer for all the other nodes.
<p>

<dd> <b>Side Effects</b> None
<p>

<dd> <b>See Also</b> <code><a href="#NodeBinaryStoreBdd">NodeBinaryStoreBdd</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreBdd.c"TARGET="ABSTRACT"><CODE>dddmpStoreBdd.c</CODE></A>

<dt><pre>
<A NAME="NumberNodeRecurAdd"></A>
static int <I></I>
<B>NumberNodeRecurAdd</B>(
  DdNode * <b>f</b>, <i>IN: root of the BDD to be numbered</i>
  int  <b>id</b> <i>IN/OUT: index to be assigned to the node</i>
)
</pre>
<dd> Number nodes recursively in post-order.
    The "visited" flag is used with inverse polarity, because all nodes
    were set "visited" when removing them from unique.
<p>

<dd> <b>Side Effects</b> "visited" flags are reset.
<p>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeAdd.c"TARGET="ABSTRACT"><CODE>dddmpNodeAdd.c</CODE></A>

<dt><pre>
<A NAME="NumberNodeRecurBdd"></A>
static int <I></I>
<B>NumberNodeRecurBdd</B>(
  DdNode * <b>f</b>, <i>IN: root of the BDD to be numbered</i>
  int  <b>id</b> <i>IN/OUT: index to be assigned to the node</i>
)
</pre>
<dd> Number nodes recursively in post-order.
    The "visited" flag is used with inverse polarity, because all nodes
    were set "visited" when removing them from unique.
<p>

<dd> <b>Side Effects</b> "visited" flags are reset.
<p>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeBdd.c"TARGET="ABSTRACT"><CODE>dddmpNodeBdd.c</CODE></A>

<dt><pre>
<A NAME="NumberNodeRecurCnf"></A>
static int <I></I>
<B>NumberNodeRecurCnf</B>(
  DdNode * <b>f</b>, <i>IN: root of the BDD to be numbered</i>
  int * <b>cnfIds</b>, <i>IN: possible source for numbering</i>
  int  <b>id</b> <i>IN/OUT: possible source for numbering</i>
)
</pre>
<dd> Number nodes recursively in post-order.
    The "visited" flag is used with inverse polarity, because all nodes
    were set "visited" when removing them from unique.
<p>

<dd> <b>Side Effects</b> "visited" flags are reset.
<p>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeCnf.c</CODE></A>

<dt><pre>
<A NAME="NumberNodeRecurCnf"></A>
static int <I></I>
<B>NumberNodeRecurCnf</B>(
  DdNode * <b>f</b>, <i>IN: root of the BDD to be numbered</i>
  int * <b>cnfIds</b>, <i>IN: possible source for numbering</i>
  int  <b>id</b> <i>IN/OUT: possible source for numbering</i>
)
</pre>
<dd> Number nodes recursively in post-order.
    The "visited" flag is used with inverse polarity, because all nodes
    were set "visited" when removing them from unique.
<p>

<dd> <b>Side Effects</b> "visited" flags are reset.
<p>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpNodeCnf.c</CODE></A>

<dt><pre>
<A NAME="NumberNodeRecur"></A>
static int <I></I>
<B>NumberNodeRecur</B>(
  DdNode * <b>f</b>, <i>IN: root of the BDD to be numbered</i>
  int  <b>id</b> <i>IN/OUT: index to be assigned to the node</i>
)
</pre>
<dd> Number nodes recursively in post-order.
    The "visited" flag is used with inverse polarity, because all nodes
    were set "visited" when removing them from unique.
<p>

<dd> <b>Side Effects</b> "visited" flags are reset.
<p>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeBdd.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeBdd.c</CODE></A>

<dt><pre>
<A NAME="QsortStrcmp"></A>
int <I></I>
<B>QsortStrcmp</B>(
  const void * <b>ps1</b>, <i>IN: pointer to the first string</i>
  const void * <b>ps2</b> <i>IN: pointer to the second string</i>
)
</pre>
<dd> String compare for qsort
<p>

<dd> <b>Side Effects</b> None
<p>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpUtil.c"TARGET="ABSTRACT"><CODE>dddmpUtil.c</CODE></A>

<dt><pre>
<A NAME="ReadByteBinary"></A>
static int <I></I>
<B>ReadByteBinary</B>(
  FILE * <b>fp</b>, <i>IN: file where to read the byte</i>
  unsigned char * <b>cp</b> <i>OUT: the read byte</i>
)
</pre>
<dd> inputs a byte to file fp. 0x00 has been used as escape character
    to filter <CR>, <LF> and <ctrl-Z>. This is done for
    compatibility between unix and dos/windows systems.
<p>

<dd> <b>Side Effects</b> None
<p>

<dd> <b>See Also</b> <code><a href="#WriteByteBinary()">WriteByteBinary()</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpBinary.c"TARGET="ABSTRACT"><CODE>dddmpBinary.c</CODE></A>

<dt><pre>
<A NAME="RemoveFromUniqueRecurAdd"></A>
static void <I></I>
<B>RemoveFromUniqueRecurAdd</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  DdNode * <b>f</b> <i>IN: root of the BDD to be extracted</i>
)
</pre>
<dd> Removes a node from the unique table by locating the proper
    subtable and unlinking the node from it. It recurs on the 
    children of the node. Constants remain untouched.
<p>

<dd> <b>Side Effects</b> Nodes are left with the "visited" flag true.
<p>

<dd> <b>See Also</b> <code><a href="#RestoreInUniqueRecurAdd">RestoreInUniqueRecurAdd</a>
()
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeAdd.c"TARGET="ABSTRACT"><CODE>dddmpNodeAdd.c</CODE></A>

<dt><pre>
<A NAME="RemoveFromUniqueRecurBdd"></A>
static void <I></I>
<B>RemoveFromUniqueRecurBdd</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  DdNode * <b>f</b> <i>IN: root of the BDD to be extracted</i>
)
</pre>
<dd> Removes a node from the unique table by locating the proper
    subtable and unlinking the node from it. It recurs on the 
    children of the node. Constants remain untouched.
<p>

<dd> <b>Side Effects</b> Nodes are left with the "visited" flag true.
<p>

<dd> <b>See Also</b> <code><a href="#RestoreInUniqueRecurBdd">RestoreInUniqueRecurBdd</a>
()
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeBdd.c"TARGET="ABSTRACT"><CODE>dddmpNodeBdd.c</CODE></A>

<dt><pre>
<A NAME="RemoveFromUniqueRecurCnf"></A>
static void <I></I>
<B>RemoveFromUniqueRecurCnf</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  DdNode * <b>f</b> <i>IN: root of the BDD to be extracted</i>
)
</pre>
<dd> Removes a node from the unique table by locating the proper
    subtable and unlinking the node from it. It recurs on  on the 
    children of the node. Constants remain untouched.
<p>

<dd> <b>Side Effects</b> Nodes are left with the "visited" flag true.
<p>

<dd> <b>See Also</b> <code><a href="#RestoreInUniqueRecurCnf()">RestoreInUniqueRecurCnf()</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpNodeCnf.c</CODE></A>

<dt><pre>
<A NAME="RemoveFromUniqueRecurCnf"></A>
static void <I></I>
<B>RemoveFromUniqueRecurCnf</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  DdNode * <b>f</b> <i>IN: root of the BDD to be extracted</i>
)
</pre>
<dd> Removes a node from the unique table by locating the proper
    subtable and unlinking the node from it. It recurs on son nodes.
<p>

<dd> <b>Side Effects</b> Nodes are left with the "visited" flag true.
<p>

<dd> <b>See Also</b> <code><a href="#RestoreInUniqueRecurCnf()">RestoreInUniqueRecurCnf()</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeCnf.c</CODE></A>

<dt><pre>
<A NAME="RemoveFromUniqueRecur"></A>
static void <I></I>
<B>RemoveFromUniqueRecur</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  DdNode * <b>f</b> <i>IN: root of the BDD to be extracted</i>
)
</pre>
<dd> Removes a node from the unique table by locating the proper
    subtable and unlinking the node from it. It recurs on the 
    children of the node.
<p>

<dd> <b>Side Effects</b> Nodes are left with the "visited" flag true.
<p>

<dd> <b>See Also</b> <code><a href="#RestoreInUniqueRecur()">RestoreInUniqueRecur()</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeBdd.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeBdd.c</CODE></A>

<dt><pre>
<A NAME="RestoreInUniqueRecurAdd"></A>
static void <I></I>
<B>RestoreInUniqueRecurAdd</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  DdNode * <b>f</b> <i>IN: root of the BDD to be restored</i>
)
</pre>
<dd> Restores a node in unique table (recursively)
<p>

<dd> <b>Side Effects</b> Nodes are not restored in the same order as before removal
<p>

<dd> <b>See Also</b> <code><a href="#RemoveFromUniqueAdd">RemoveFromUniqueAdd</a>
()
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeAdd.c"TARGET="ABSTRACT"><CODE>dddmpNodeAdd.c</CODE></A>

<dt><pre>
<A NAME="RestoreInUniqueRecurBdd"></A>
static void <I></I>
<B>RestoreInUniqueRecurBdd</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  DdNode * <b>f</b> <i>IN: root of the BDD to be restored</i>
)
</pre>
<dd> Restores a node in unique table (recursively)
<p>

<dd> <b>Side Effects</b> Nodes are not restored in the same order as before removal
<p>

<dd> <b>See Also</b> <code><a href="#RemoveFromUnique()">RemoveFromUnique()</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeBdd.c"TARGET="ABSTRACT"><CODE>dddmpNodeBdd.c</CODE></A>

<dt><pre>
<A NAME="RestoreInUniqueRecurCnf"></A>
static void <I></I>
<B>RestoreInUniqueRecurCnf</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  DdNode * <b>f</b> <i>IN: root of the BDD to be restored</i>
)
</pre>
<dd> Restores a node in unique table (recursive)
<p>

<dd> <b>Side Effects</b> Nodes are not restored in the same order as before removal
<p>

<dd> <b>See Also</b> <code><a href="#RemoveFromUnique()">RemoveFromUnique()</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeCnf.c</CODE></A>

<dt><pre>
<A NAME="RestoreInUniqueRecurCnf"></A>
static void <I></I>
<B>RestoreInUniqueRecurCnf</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  DdNode * <b>f</b> <i>IN: root of the BDD to be restored</i>
)
</pre>
<dd> Restores a node in unique table (recursive)
<p>

<dd> <b>Side Effects</b> Nodes are not restored in the same order as before removal
<p>

<dd> <b>See Also</b> <code><a href="#RemoveFromUnique()">RemoveFromUnique()</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpNodeCnf.c"TARGET="ABSTRACT"><CODE>dddmpNodeCnf.c</CODE></A>

<dt><pre>
<A NAME="RestoreInUniqueRecur"></A>
static void <I></I>
<B>RestoreInUniqueRecur</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  DdNode * <b>f</b> <i>IN: root of the BDD to be restored</i>
)
</pre>
<dd> Restores a node in unique table (recursively)
<p>

<dd> <b>Side Effects</b> Nodes are not restored in the same order as before removal
<p>

<dd> <b>See Also</b> <code><a href="#RemoveFromUnique()">RemoveFromUnique()</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpDdNodeBdd.c"TARGET="ABSTRACT"><CODE>dddmpDdNodeBdd.c</CODE></A>

<dt><pre>
<A NAME="StoreCnfBestNotSharedRecur"></A>
static int <I></I>
<B>StoreCnfBestNotSharedRecur</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  DdNode * <b>node</b>, <i>IN: BDD to store</i>
  int  <b>idf</b>, <i>IN: Id to store</i>
  int * <b>bddIds</b>, <i>IN: BDD identifiers</i>
  int * <b>cnfIds</b>, <i>IN: corresponding CNF identifiers</i>
  FILE * <b>fp</b>, <i>IN: file pointer</i>
  int * <b>list</b>, <i>IN: temporary array to store cubes</i>
  int * <b>clauseN</b>, <i>OUT: number of stored clauses</i>
  int * <b>varMax</b> <i>OUT: maximum identifier of the variables created</i>
)
</pre>
<dd> Performs the recursive step of Print Best on Not Shared
    sub-BDDs, i.e., print out information for the nodes belonging to
    BDDs not shared (whose root has just one incoming edge).
<p>

<dd> <b>Side Effects</b> None
<p>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreCnf.c"TARGET="ABSTRACT"><CODE>dddmpStoreCnf.c</CODE></A>

<dt><pre>
<A NAME="StoreCnfBestSharedRecur"></A>
static int <I></I>
<B>StoreCnfBestSharedRecur</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  DdNode * <b>node</b>, <i>IN: BDD to store</i>
  int * <b>bddIds</b>, <i>IN: BDD identifiers</i>
  int * <b>cnfIds</b>, <i>IN: corresponding CNF identifiers</i>
  FILE * <b>fp</b>, <i>IN: file pointer</i>
  int * <b>list</b>, <i>IN: temporary array to store cubes</i>
  int * <b>clauseN</b>, <i>OUT: number of stored clauses</i>
  int * <b>varMax</b> <i>OUT: maximum identifier of the variables created</i>
)
</pre>
<dd> Performs the recursive step of Print Best on Not Shared
    sub-BDDs, i.e., print out information for the nodes belonging to
    BDDs not shared (whose root has just one incoming edge).
<p>

<dd> <b>Side Effects</b> None
<p>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreCnf.c"TARGET="ABSTRACT"><CODE>dddmpStoreCnf.c</CODE></A>

<dt><pre>
<A NAME="StoreCnfBest"></A>
static int <I></I>
<B>StoreCnfBest</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  DdNode ** <b>f</b>, <i>IN: array of BDDs to store</i>
  int  <b>rootN</b>, <i>IN: number of BDD in the array</i>
  int * <b>bddIds</b>, <i>IN: BDD identifiers</i>
  int * <b>cnfIds</b>, <i>IN: corresponding CNF identifiers</i>
  int  <b>idInitial</b>, <i>IN: initial value for numbering new CNF variables</i>
  FILE * <b>fp</b>, <i>IN: file pointer</i>
  int * <b>varMax</b>, <i>OUT: maximum identifier of the variables created</i>
  int * <b>clauseN</b>, <i>OUT: number of stored clauses</i>
  int * <b>rootStartLine</b> <i>OUT: line where root starts</i>
)
</pre>
<dd> Prints a disjoint sum of product cover for the function
    rooted at node intorducing cutting points whenever necessary.
    Each product corresponds to a path from node a leaf
    node different from the logical zero, and different from the
    background value. Uses the standard output.  Returns 1 if 
    successful, 0 otherwise.
<p>

<dd> <b>Side Effects</b> None
<p>

<dd> <b>See Also</b> <code><a href="#StoreCnfMaxtermByMaxterm">StoreCnfMaxtermByMaxterm</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreCnf.c"TARGET="ABSTRACT"><CODE>dddmpStoreCnf.c</CODE></A>

<dt><pre>
<A NAME="StoreCnfMaxtermByMaxtermRecur"></A>
static void <I></I>
<B>StoreCnfMaxtermByMaxtermRecur</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  DdNode * <b>node</b>, <i>IN: BDD to store</i>
  int * <b>bddIds</b>, <i>IN: BDD identifiers</i>
  int * <b>cnfIds</b>, <i>IN: corresponding CNF identifiers</i>
  FILE * <b>fp</b>, <i>IN: file pointer</i>
  int * <b>list</b>, <i>IN: temporary array to store cubes</i>
  int * <b>clauseN</b>, <i>OUT: number of stored clauses</i>
  int * <b>varMax</b> <i>OUT: maximum identifier of the variables created</i>
)
</pre>
<dd> Performs the recursive step of Print Maxterm.
    Traverse a BDD a print out a cube in CNF format each time a terminal
    node is reached.
<p>

<dd> <b>Side Effects</b> None
<p>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreCnf.c"TARGET="ABSTRACT"><CODE>dddmpStoreCnf.c</CODE></A>

<dt><pre>
<A NAME="StoreCnfMaxtermByMaxterm"></A>
static int <I></I>
<B>StoreCnfMaxtermByMaxterm</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  DdNode ** <b>f</b>, <i>IN: array of BDDs to store</i>
  int  <b>rootN</b>, <i>IN: number of BDDs in the array</i>
  int * <b>bddIds</b>, <i>IN: BDD Identifiers</i>
  int * <b>cnfIds</b>, <i>IN: corresponding CNF Identifiers</i>
  int  <b>idInitial</b>, <i>IN: initial value for numbering new CNF variables</i>
  FILE * <b>fp</b>, <i>IN: file pointer</i>
  int * <b>varMax</b>, <i>OUT: maximum identifier of the variables created</i>
  int * <b>clauseN</b>, <i>OUT: number of stored clauses</i>
  int * <b>rootStartLine</b> <i>OUT: line where root starts</i>
)
</pre>
<dd> Prints a disjoint sum of product cover for the function
    rooted at node. Each product corresponds to a path from node a 
    leaf node different from the logical zero, and different from 
    the background value. Uses the standard output.  Returns 1 if 
    successful, 0 otherwise.
<p>

<dd> <b>Side Effects</b> None
<p>

<dd> <b>See Also</b> <code><a href="#StoreCnfBest">StoreCnfBest</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreCnf.c"TARGET="ABSTRACT"><CODE>dddmpStoreCnf.c</CODE></A>

<dt><pre>
<A NAME="StoreCnfNodeByNodeRecur"></A>
static int <I></I>
<B>StoreCnfNodeByNodeRecur</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  DdNode * <b>f</b>, <i>IN: BDD node to be stored</i>
  int * <b>bddIds</b>, <i>IN: BDD ids for variables</i>
  int * <b>cnfIds</b>, <i>IN: CNF ids for variables</i>
  FILE * <b>fp</b>, <i>IN: store file</i>
  int * <b>clauseN</b>, <i>OUT: number of clauses written in the CNF file</i>
  int * <b>varMax</b> <i>OUT: maximum value of id written in the CNF file</i>
)
</pre>
<dd> Performs the recursive step of Dddmp_bddStore.
    Traverse the BDD and store a CNF formula for each "terminal" node.
<p>

<dd> <b>Side Effects</b> None
<p>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreCnf.c"TARGET="ABSTRACT"><CODE>dddmpStoreCnf.c</CODE></A>

<dt><pre>
<A NAME="StoreCnfNodeByNode"></A>
static int <I></I>
<B>StoreCnfNodeByNode</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  DdNode ** <b>f</b>, <i>IN: BDD array to be stored</i>
  int  <b>rootN</b>, <i>IN: number of BDDs in the array</i>
  int * <b>bddIds</b>, <i>IN: BDD ids for variables</i>
  int * <b>cnfIds</b>, <i>IN: CNF ids for variables</i>
  FILE * <b>fp</b>, <i>IN: store file</i>
  int * <b>clauseN</b>, <i>IN/OUT: number of clauses written in the CNF file</i>
  int * <b>varMax</b>, <i>IN/OUT: maximum value of id written in the CNF file</i>
  int * <b>rootStartLine</b> <i>OUT: CNF line where root starts</i>
)
</pre>
<dd> Store the BDD as CNF clauses.
    Use a multiplexer description for each BDD node.
<p>

<dd> <b>Side Effects</b> None
<p>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreCnf.c"TARGET="ABSTRACT"><CODE>dddmpStoreCnf.c</CODE></A>

<dt><pre>
<A NAME="StoreCnfOneNode"></A>
static int <I></I>
<B>StoreCnfOneNode</B>(
  DdNode * <b>f</b>, <i>IN: node to be stored</i>
  int  <b>idf</b>, <i>IN: node CNF Index</i>
  int  <b>vf</b>, <i>IN: node BDD Index</i>
  int  <b>idT</b>, <i>IN: Then CNF Index with sign = inverted edge</i>
  int  <b>idE</b>, <i>IN: Else CNF Index with sign = inverted edge</i>
  FILE * <b>fp</b>, <i>IN: store file</i>
  int * <b>clauseN</b>, <i>OUT: number of clauses</i>
  int * <b>varMax</b> <i>OUT: maximun Index of variable stored</i>
)
</pre>
<dd> Store One Single BDD Node translating it as a multiplexer.
<p>

<dd> <b>Side Effects</b> None
<p>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreCnf.c"TARGET="ABSTRACT"><CODE>dddmpStoreCnf.c</CODE></A>

<dt><pre>
<A NAME="WriteByteBinary"></A>
static int <I></I>
<B>WriteByteBinary</B>(
  FILE * <b>fp</b>, <i>IN: file where to write the byte</i>
  unsigned char  <b>c</b> <i>IN: the byte to be written</i>
)
</pre>
<dd> outputs a byte to file fp. Uses 0x00 as escape character
    to filter <CR>, <LF> and <ctrl-Z>.
    This is done for compatibility between unix and dos/windows systems.
<p>

<dd> <b>Side Effects</b> None
<p>

<dd> <b>See Also</b> <code><a href="#ReadByteBinary()">ReadByteBinary()</a>
</code>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpBinary.c"TARGET="ABSTRACT"><CODE>dddmpBinary.c</CODE></A>

<dt><pre>
<A NAME="printCubeCnf"></A>
static int <I></I>
<B>printCubeCnf</B>(
  DdManager * <b>ddMgr</b>, <i>IN: DD Manager</i>
  DdNode * <b>node</b>, <i>IN: BDD to store</i>
  int * <b>cnfIds</b>, <i>IN: CNF identifiers</i>
  FILE * <b>fp</b>, <i>IN: file pointer</i>
  int * <b>list</b>, <i>IN: temporary array to store cubes</i>
  int * <b>varMax</b> <i>OUT: maximum identifier of the variables created</i>
)
</pre>
<dd> Print One Cube in CNF Format.
    Return DDDMP_SUCCESS if something is printed out, DDDMP_FAILURE
    is nothing is printed out.
<p>

<dd> <b>Side Effects</b> None
<p>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpStoreCnf.c"TARGET="ABSTRACT"><CODE>dddmpStoreCnf.c</CODE></A>

<dt><pre>
<A NAME=""></A>
 <I></I>
<B></B>(
   <b></b> <i></i>
)
</pre>
<dd> Checks for Warnings: If expr==1 it prints out the warning
    on stderr.
<p>

<dd> <b>Side Effects</b> None
<p>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmp.h"TARGET="ABSTRACT"><CODE>dddmp.h</CODE></A>

<dt><pre>
<A NAME=""></A>
 <I></I>
<B></B>(
   <b></b> <i></i>
)
</pre>
<dd> Checks for fatal bugs and go to the label to deal with
    the error.
<p>

<dd> <b>Side Effects</b> None
<p>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmp.h"TARGET="ABSTRACT"><CODE>dddmp.h</CODE></A>

<dt><pre>
<A NAME=""></A>
 <I></I>
<B></B>(
   <b></b> <i></i>
)
</pre>
<dd> Checks for fatal bugs and return the DDDMP_FAILURE flag.
<p>

<dd> <b>Side Effects</b> None
<p>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmp.h"TARGET="ABSTRACT"><CODE>dddmp.h</CODE></A>

<dt><pre>
<A NAME=""></A>
 <I></I>
<B></B>(
   <b></b> <i></i>
)
</pre>
<dd> Conditional safety assertion. It prints out the file
    name and line number where the fatal error occurred.
    Messages are printed out on stderr.
<p>

<dd> <b>Side Effects</b> None
<p>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmp.h"TARGET="ABSTRACT"><CODE>dddmp.h</CODE></A>

<dt><pre>
<A NAME=""></A>
 <I></I>
<B></B>(
   <b></b> <i></i>
)
</pre>
<dd> Memory Allocation Macro for DDDMP
<p>

<dd> <b>Side Effects</b> None
<p>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpInt.h"TARGET="ABSTRACT"><CODE>dddmpInt.h</CODE></A>

<dt><pre>
<A NAME=""></A>
 <I></I>
<B></B>(
   <b></b> <i></i>
)
</pre>
<dd> Memory Free Macro for DDDMP
<p>

<dd> <b>Side Effects</b> None
<p>

<DD> <B>Defined in </B> <A HREF="dddmpAllFile.html#dddmpInt.h"TARGET="ABSTRACT"><CODE>dddmpInt.h</CODE></A>


</DL>
<HR>
Last updated on 1040218 17h14
</BODY></HTML>
